[mc] Documentation cleanup

diff --git a/src/mc/Channel.hpp b/src/mc/Channel.hpp
index 64219c4..30e03c6 100644 (file)
--- a/src/mc/Channel.hpp
+++ b/src/mc/Channel.hpp
@@ -18,8 +18,8 @@ namespace mc {
 
 /** A channel for exchanging messages between model-checker and model-checked
  *
 
 /** A channel for exchanging messages between model-checker and model-checked
  *

- *  This hides the way the messages are transferred. Currently, they are sent
- *  over a SOCK_DGRAM socket.
+ *  This abstracts away the way the messages are transferred. Currently, they
+ *  are sent over a (connected) `SOCK_DGRAM` socket.

  */
 class Channel {
   int socket_ = -1;
  */
 class Channel {
   int socket_ = -1;

diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp
index 70a9031..4575439 100644 (file)
--- a/src/mc/Checker.hpp
+++ b/src/mc/Checker.hpp
@@ -20,13 +20,16 @@ namespace mc {
 
 /** A model-checking algorithm
  *
 
 /** A model-checking algorithm
  *

- *  The goal is to move the data/state/configuration of a model-checking
- *  algorithms in subclasses. Implementing this interface will probably
- *  not be really mandatory, you might be able to write your
- *  model-checking algorithm as plain imperative code instead.
+ *  This is an abstract base class used to group the data, state, configuration
+ *  of a model-checking algorithm.

  *
  *

- *  It works by manipulating a model-checking Session.
- */
+ *  Implementing this interface will probably not be really mandatory,
+ *  you might be able to write your model-checking algorithm as plain
+ *  imperative code instead.
+ *
+ *  It is expected to interact with the model-checking core through the
+ * `Session` interface (but currently the `Session` interface does not
+ *  have all the necessary features). */

 // abstract
 class Checker {
   Session* session_;
 // abstract
 class Checker {
   Session* session_;


@@ -38,16 +41,23 @@ public:
   Checker& operator=(Checker const&) = delete;
 
   virtual ~Checker();
   Checker& operator=(Checker const&) = delete;
 
   virtual ~Checker();

+
+  /** Main function of this algorithm */

   virtual int run() = 0;
 
   virtual int run() = 0;
 

-  // Give me your internal state:
+  /* These methods are callbacks called by the model-checking engine
+   * to get and display information about the current state of the
+   * model-checking algorithm: */

 
   /** Show the current trace/stack
    *
 
   /** Show the current trace/stack
    *

-   *  Could this be handled in the Session/ModelChecker instead?
-   */
+   *  Could this be handled in the Session/ModelChecker instead? */

   virtual RecordTrace getRecordTrace();
   virtual RecordTrace getRecordTrace();

+
+  /** Generate a textual execution trace of the simulated application */

   virtual std::vector<std::string> getTextualTrace();
   virtual std::vector<std::string> getTextualTrace();

+
+  /** Log additional information about the state of the model-checker */

   virtual void logState();
 
 protected:
   virtual void logState();
 
 protected:

diff --git a/src/mc/ChunkedData.hpp b/src/mc/ChunkedData.hpp
index ae6efb1..076e607 100644 (file)
--- a/src/mc/ChunkedData.hpp
+++ b/src/mc/ChunkedData.hpp
@@ -19,10 +19,19 @@
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {
 

-/** A byte-string represented as a sequence of chunks from a PageStor */
+/** A byte-string represented as a sequence of chunks from a PageStore
+ *
+ *  In order to save memory when taking memory snapshots, a given byte-string
+ *  is split in fixed-size chunks. Identical chunks (either from the same
+ *  snapshot or more probably from different snpashots) share the same memory
+ *  storage.
+ *
+ *  Thus a chunked is represented as a sequence of indices of each chunk.
+ */

 class ChunkedData {
 class ChunkedData {

+  /** This is where we store the chunks */

   PageStore* store_ = nullptr;
   PageStore* store_ = nullptr;

-  /** Indices of the chunks */
+  /** Indices of the chunks in the `PageStore` */

   std::vector<std::size_t> pagenos_;
 public:
 
   std::vector<std::size_t> pagenos_;
 public:
 


@@ -72,10 +81,16 @@ public:
     return *this;
   }
 
     return *this;
   }
 

+  /** How many pages are used */

   std::size_t page_count()          const { return pagenos_.size(); }
   std::size_t page_count()          const { return pagenos_.size(); }

+
+  /** Get a chunk index */

   std::size_t pageno(std::size_t i) const { return pagenos_[i]; }
   std::size_t pageno(std::size_t i) const { return pagenos_[i]; }

+
+  /** Get a view of the chunk indices */

   const std::size_t* pagenos()      const { return pagenos_.data(); }
 
   const std::size_t* pagenos()      const { return pagenos_.data(); }
 

+  /** Get a a pointer to a chunk */

   const void* page(std::size_t i) const
   {
     return store_->get_page(pagenos_[i]);
   const void* page(std::size_t i) const
   {
     return store_->get_page(pagenos_[i]);

diff --git a/src/mc/DwarfExpression.hpp b/src/mc/DwarfExpression.hpp
index 4f16164..1e23242 100644 (file)
--- a/src/mc/DwarfExpression.hpp
+++ b/src/mc/DwarfExpression.hpp
@@ -19,9 +19,9 @@
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/AddressSpace.hpp"
 
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/AddressSpace.hpp"
 

-/** @file DwarfExession.hpp
+/** @file DwarfExpression.hpp

  *
  *

- *  Evaluation of DWARF location expressions
+ *  Evaluation of DWARF location expressions.

  */
 
 namespace simgrid {
  */
 
 namespace simgrid {


@@ -30,7 +30,7 @@ namespace dwarf {
 /** A DWARF expression
  *
  *  DWARF defines a simple stack-based VM for evaluating expressions
 /** A DWARF expression
  *
  *  DWARF defines a simple stack-based VM for evaluating expressions

- *  (such as locations of variables, etc.): A DWARF expressions is
+ *  (such as locations of variables, etc.): a DWARF expressions is

  *  just a sequence of dwarf instructions. We currently directly use
  *  `Dwarf_Op` from `dwarf.h` for dwarf instructions.
  */
  *  just a sequence of dwarf instructions. We currently directly use
  *  `Dwarf_Op` from `dwarf.h` for dwarf instructions.
  */


@@ -71,6 +71,7 @@ public:
   typedef std::uintptr_t value_type;
   static const std::size_t max_size = 64;
 private:
   typedef std::uintptr_t value_type;
   static const std::size_t max_size = 64;
 private:

+  // Values of the stack (the top is stack_[size_ - 1]):

   uintptr_t stack_[max_size];
   size_t size_;
 public:
   uintptr_t stack_[max_size];
   size_t size_;
 public:


@@ -103,7 +104,7 @@ public:
   void push(value_type value)
   {
     if (size_ == max_size)
   void push(value_type value)
   {
     if (size_ == max_size)

-      throw evaluation_error("Dwarf stack overflow");
+      throw evaluation_error("DWARF stack overflow");

     stack_[size_++] = value;
   }
 
     stack_[size_++] = value;
   }
 


@@ -111,7 +112,7 @@ public:
   value_type pop()
   {
     if (size_ == 0)
   value_type pop()
   {
     if (size_ == 0)

-      throw evaluation_error("Stack underflow");
+      throw evaluation_error("DWARF stack underflow");

     return stack_[--size_];
   }
 
     return stack_[--size_];
   }
 

diff --git a/src/mc/Frame.cpp b/src/mc/Frame.cpp
index 40f9ed3..135b79c 100644 (file)
--- a/src/mc/Frame.cpp
+++ b/src/mc/Frame.cpp
@@ -22,8 +22,8 @@ void* Frame::frame_base(unw_cursor_t& unw_cursor) const
     return location.address();
   else if (location.in_register()) {
     // This is a special case.
     return location.address();
   else if (location.in_register()) {
     // This is a special case.

-    // The register if not the location of the frame base
-    // (a frame base cannot be located in a register)
+    // The register is not the location of the frame base
+    // (a frame base cannot be located in a register).

     // Instead, DWARF defines this to mean that the register
     // contains the address of the frame base.
     unw_word_t word;
     // Instead, DWARF defines this to mean that the register
     // contains the address of the frame base.
     unw_word_t word;

diff --git a/src/mc/LocationList.hpp b/src/mc/LocationList.hpp
index 52efb5b..830f024 100644 (file)
--- a/src/mc/LocationList.hpp
+++ b/src/mc/LocationList.hpp
@@ -25,12 +25,13 @@
 namespace simgrid {
 namespace dwarf {
 
 namespace simgrid {
 namespace dwarf {
 

-/** \brief A DWARF expression with optional validity constraints */
+/** A DWARF expression with optional validity constraints */

 class LocationListEntry {
 public:
   typedef simgrid::xbt::Range<std::uint64_t> range_type;
 private:
   DwarfExpression expression_;
 class LocationListEntry {
 public:
   typedef simgrid::xbt::Range<std::uint64_t> range_type;
 private:
   DwarfExpression expression_;

+  // By default, the expression is always valid:

   range_type range_ = {0, UINT64_MAX};
 public:
   LocationListEntry() {}
   range_type range_ = {0, UINT64_MAX};
 public:
   LocationListEntry() {}

diff --git a/src/mc/mc_record.h b/src/mc/mc_record.h
index 7901b67..ec24b70 100644 (file)
--- a/src/mc/mc_record.h
+++ b/src/mc/mc_record.h
@@ -4,7 +4,8 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 

-/** \file
+/** \file mc_record.h
+ *

  *  This file contains the MC replay/record functionnality.
  *  A MC path may be recorded by using ``-cfg=model-check/record:1`'`.
  *  The path is written in the log output and an be replayed with MC disabled
  *  This file contains the MC replay/record functionnality.
  *  A MC path may be recorded by using ``-cfg=model-check/record:1`'`.
  *  The path is written in the log output and an be replayed with MC disabled

diff --git a/src/mc/mc_replay.h b/src/mc/mc_replay.h
index d92703c..f9324c8 100644 (file)
--- a/src/mc/mc_replay.h
+++ b/src/mc/mc_replay.h
@@ -4,8 +4,6 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 

-/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
-

 #ifndef SIMGRID_MC_REPLAY_H
 #define SIMGRID_MC_REPLAY_H
 
 #ifndef SIMGRID_MC_REPLAY_H
 #define SIMGRID_MC_REPLAY_H