From a6683a1cd7515c04a74364c9f991d55d9329a7c5 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 18 Jul 2016 16:12:37 +0200 Subject: [PATCH] [mc] Documentation cleanup --- src/mc/Channel.hpp | 4 ++-- src/mc/Checker.hpp | 28 +++++++++++++++++++--------- src/mc/ChunkedData.hpp | 19 +++++++++++++++++-- src/mc/DwarfExpression.hpp | 11 ++++++----- src/mc/Frame.cpp | 4 ++-- src/mc/LocationList.hpp | 3 ++- src/mc/mc_record.h | 3 ++- src/mc/mc_replay.h | 2 -- 8 files changed, 50 insertions(+), 24 deletions(-) diff --git a/src/mc/Channel.hpp b/src/mc/Channel.hpp index 64219c4eac..30e03c6b1f 100644 --- 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 * - * 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; diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp index 70a9031b86..4575439965 100644 --- a/src/mc/Checker.hpp +++ b/src/mc/Checker.hpp @@ -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 getTextualTrace(); + + /** Log additional information about the state of the model-checker */ virtual void logState(); protected: diff --git a/src/mc/ChunkedData.hpp b/src/mc/ChunkedData.hpp index ae6efb13e5..076e607560 100644 --- a/src/mc/ChunkedData.hpp +++ b/src/mc/ChunkedData.hpp @@ -19,10 +19,19 @@ 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 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]); diff --git a/src/mc/DwarfExpression.hpp b/src/mc/DwarfExpression.hpp index 4f1616440e..1e2324299e 100644 --- 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" -/** @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_]; } diff --git a/src/mc/Frame.cpp b/src/mc/Frame.cpp index 40f9ed363a..135b79cf57 100644 --- 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. - // 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; diff --git a/src/mc/LocationList.hpp b/src/mc/LocationList.hpp index 52efb5bc5d..830f02437e 100644 --- a/src/mc/LocationList.hpp +++ b/src/mc/LocationList.hpp @@ -25,12 +25,13 @@ 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 range_type; private: DwarfExpression expression_; + // By default, the expression is always valid: range_type range_ = {0, UINT64_MAX}; public: LocationListEntry() {} diff --git a/src/mc/mc_record.h b/src/mc/mc_record.h index 7901b67e07..ec24b70d49 100644 --- 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. */ -/** \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 diff --git a/src/mc/mc_replay.h b/src/mc/mc_replay.h index d92703c180..f9324c8f27 100644 --- 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. */ -/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid */ - #ifndef SIMGRID_MC_REPLAY_H #define SIMGRID_MC_REPLAY_H -- 2.20.1