diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/MergeHandler.h | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h index 79357d7c..75f4a3d1 100644 --- a/include/klee/MergeHandler.h +++ b/include/klee/MergeHandler.h @@ -48,6 +48,22 @@ * reaches zero, every state which ran into the same `klee_open_merge()` is now * paused and waiting to be merged. The destructor of the MergeHandler * then continues the scheduling of the corresponding paused states. + * + * # Non-blocking State Merging + * + * This feature adds functionality to the BoundedMergingSearcher that will + * prioritize (e.g., immediately schedule) states running inside a bounded-merge + * region once a state has reached a corresponding klee_close_merge() call. The + * goal is to quickly gather all states inside the merging region in order to + * release the waiting states. However, states that are running for more than + * twice the mean number of instructions compared to the states that are already + * waiting, will not be prioritized anymore. + * + * Once no more states are available for prioritizing, but there are states + * waiting to be released, these states (which have already been merged as good as + * possible) will be continued without waiting for the remaining states. When a + * remaining state now enters a close-merge point, it will again wait for the + * other states, or until the 'timeout' is reached. */ #ifndef KLEE_MERGEHANDLER_H @@ -85,14 +101,14 @@ private: /// @brief The average number of instructions between the open and close merge of each /// state that has finished so far - double closeMean; + double closedMean; /// @brief Number of states that are tracked by this MergeHandler, that ran /// into a relevant klee_close_merge unsigned closedStateCount; /// @brief Get distance of state from the openInstruction - unsigned getInstrDistance(ExecutionState *es); + unsigned getInstructionDistance(ExecutionState *es); /// @brief States that ran through the klee_open_merge, but not yet into a /// corresponding klee_close_merge @@ -101,7 +117,7 @@ private: /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into /// them std::map<llvm::Instruction *, std::vector<ExecutionState *> > - reachedMergeClose; + reachedCloseMerge; public: |