Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Documentation cleanup
authorGabriel Corona <gabriel.corona@loria.fr>
Mon, 18 Jul 2016 14:12:37 +0000 (16:12 +0200)
committerGabriel Corona <gabriel.corona@loria.fr>
Mon, 18 Jul 2016 14:34:16 +0000 (16:34 +0200)
src/mc/Channel.hpp
src/mc/Checker.hpp
src/mc/ChunkedData.hpp
src/mc/DwarfExpression.hpp
src/mc/Frame.cpp
src/mc/LocationList.hpp
src/mc/mc_record.h
src/mc/mc_replay.h

index 64219c4..30e03c6 100644 (file)
@@ -18,8 +18,8 @@ namespace mc {
 
 /** 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;
index 70a9031..4575439 100644 (file)
@@ -20,13 +20,16 @@ namespace mc {
 
 /** 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_;
@@ -38,16 +41,23 @@ public:
   Checker& operator=(Checker const&) = delete;
 
   virtual ~Checker();
+
+  /** Main function of this algorithm */
   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
    *
-   *  Could this be handled in the Session/ModelChecker instead?
-   */
+   *  Could this be handled in the Session/ModelChecker instead? */
   virtual RecordTrace getRecordTrace();
+
+  /** Generate a textual execution trace of the simulated application */
   virtual std::vector<std::string> getTextualTrace();
+
+  /** Log additional information about the state of the model-checker */
   virtual void logState();
 
 protected:
index ae6efb1..076e607 100644 (file)
 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 {
+  /** This is where we store the chunks */
   PageStore* store_ = nullptr;
-  /** Indices of the chunks */
+  /** Indices of the chunks in the `PageStore` */
   std::vector<std::size_t> pagenos_;
 public:
 
@@ -72,10 +81,16 @@ public:
     return *this;
   }
 
+  /** How many pages are used */
   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]; }
+
+  /** Get a view of the chunk indices */
   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]);
index 4f16164..1e23242 100644 (file)
@@ -19,9 +19,9 @@
 #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 {
@@ -30,7 +30,7 @@ namespace dwarf {
 /** 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.
  */
@@ -71,6 +71,7 @@ public:
   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:
@@ -103,7 +104,7 @@ public:
   void push(value_type value)
   {
     if (size_ == max_size)
-      throw evaluation_error("Dwarf stack overflow");
+      throw evaluation_error("DWARF stack overflow");
     stack_[size_++] = value;
   }
 
@@ -111,7 +112,7 @@ public:
   value_type pop()
   {
     if (size_ == 0)
-      throw evaluation_error("Stack underflow");
+      throw evaluation_error("DWARF stack underflow");
     return stack_[--size_];
   }
 
index 40f9ed3..135b79c 100644 (file)
@@ -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.
-    // 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;
index 52efb5b..830f024 100644 (file)
 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_;
+  // By default, the expression is always valid:
   range_type range_ = {0, UINT64_MAX};
 public:
   LocationListEntry() {}
index 7901b67..ec24b70 100644 (file)
@@ -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. */
 
-/** \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
index d92703c..f9324c8 100644 (file)
@@ -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. */
 
-/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
-
 #ifndef SIMGRID_MC_REPLAY_H
 #define SIMGRID_MC_REPLAY_H