public:
std::shared_ptr<simgrid::mc::Snapshot> parent_snapshot_;
-public:
ModelChecker(ModelChecker const&) = delete;
ModelChecker& operator=(ModelChecker const&) = delete;
explicit ModelChecker(std::unique_ptr<RemoteClient> process);
class PageStore {
public: // Types
typedef std::uint64_t hash_type;
-private: // Types
+
+private:
+ // Types
// We are using a cheap hash to index a page.
// We should expect collision and we need to associate multiple page indices
// to the same hash.
typedef std::unordered_set<std::size_t> page_set_type;
typedef std::unordered_map<hash_type, page_set_type> pages_map_type;
-private: // Fields:
+ // Fields:
/** First page */
void* memory_;
/** Number of available pages in virtual memory */
/** Index from page hash to page index */
pages_map_type hash_index_;
-private: // Methods
+ // Methods
void resize(std::size_t size);
std::size_t alloc_page();
void remove_page(std::size_t pageno);
-public: // Constructors
+public:
+ // Constructors
PageStore(PageStore const&) = delete;
PageStore& operator=(PageStore const&) = delete;
explicit PageStore(std::size_t size);
~PageStore();
-public: // Methods
+ // Methods
/** @brief Decrement the reference count for a given page
*
*/
const void* get_page(std::size_t pageno) const;
-public: // Debug/test methods
+ // Debug/test methods
/** @brief Get the number of references for a page */
std::size_t get_ref(std::size_t pageno);
void* data_ = nullptr;
std::size_t size_;
Type type_ = Type::Malloc;
-private:
+
Buffer(std::size_t size, Type type = Type::Malloc);
Buffer(void* data, std::size_t size, Type type = Type::Malloc) :
data_(data), size_(size), type_(type) {}
-/* Copyright (c) 2016. The SimGrid Team.
+/* Copyright (c) 2016-2017. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
std::unique_ptr<ModelChecker> modelChecker_;
std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
-private:
Session(pid_t pid, int socket);
// No copy:
~Session();
void close();
-public:
void initialize();
void execute(Transition const& transition);
void logState();
void restoreInitialState();
-public: // static constructors
+ // static constructors
/** Create a new session by forking
*
void purgeVisitedPairs();
void backtrack();
std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions);
-private:
+
// A stack of (application_state, automaton_state) pairs for DFS exploration:
std::list<std::shared_ptr<Pair>> explorationStack_;
std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
void checkNonTermination(simgrid::mc::State* current_state);
void backtrack();
void restoreState();
-private:
+
/** Stack representing the position in the exploration graph */
std::list<std::unique_ptr<simgrid::mc::State>> stack_;
simgrid::mc::VisitedStates visitedStates_;
void refresh_malloc_info();
void refresh_simix();
-private:
pid_t pid_ = -1;
Channel channel_;
bool running_ = false;
std::vector<s_stack_region_t> stack_areas_;
std::vector<IgnoredHeapRegion> ignored_heap_;
-public: // object info
+public:
+ // object info
// TODO, make private (first, objectify simgrid::mc::ObjectInformation*)
std::vector<std::shared_ptr<simgrid::mc::ObjectInformation>> object_infos;
std::shared_ptr<simgrid::mc::ObjectInformation> libsimgrid_info;
std::shared_ptr<simgrid::mc::ObjectInformation> binary_info;
-public: // Copies of MCed SMX data structures
- /** Copy of `simix_global->process_list`
- *
- * See mc_smx.c.
- */
+ // Copies of MCed SMX data structures
+ /** Copy of `simix_global->process_list`
+ *
+ * See mc_smx.c.
+ */
std::vector<ActorInformation> smx_actors_infos;
/** Copy of `simix_global->process_to_destroy`
*/
std::vector<malloc_info> heap_info;
-public: // Libunwind-data
- /** Full-featured MC-aware libunwind address space for the process
- *
- * This address space is using a simgrid::mc::UnwindContext*
- * (with simgrid::mc::Process* / simgrid::mc::AddressSpace*
- * and unw_context_t).
- */
+ // Libunwind-data
+ /** Full-featured MC-aware libunwind address space for the process
+ *
+ * This address space is using a simgrid::mc::UnwindContext*
+ * (with simgrid::mc::Process* / simgrid::mc::AddressSpace*
+ * and unw_context_t).
+ */
unw_addr_space_t unw_addr_space;
/** Underlying libunwind address-space
