Tags: mcminickpt/mcmini
Tags
Version 0.0.3 Version 0.0.3 includes support for reader -writer locks, double-writer locks, and different wake-up policies for condition variables.
McMini Version 0.0.2 McMini version 0.0.2 adds the ability for transition subclasses to support _state reversal_. If a transition is revertible, you can now mark that transition as such and implement the `MCTransition::unapplyTo(MCState *)` method. McMini uses this information to determine if, when possible, it can simply revert transitions from the top of the transition stack instead of replaying transitions from the bottom of the stack and re-initializing all visible object states. The project structure of McMini has also been altered a fair bit to improve readability by splitting the header files and implementation files into two separate directories.
McMini Version 0.0.1 includes support McMini version 0.0.1 includes built-in support for model checking the following primitives: pthread_t pthread_barrier_t pthread_cond_t pthread_mutex_t sem_t McMini also supports detecting data races between simple shared variables using the READ(x) and WRITE(x) macros which expand to explicit calls to mcmini wrapper functions for reading and writing shared variables, though this support is still limited to simple data types. Version 0.0.1 uses clock vectors to determine the "happens-before" relation between events in the transition stack quickly, albeit with some overhead when the transition stack grows.
McMini-0.0.1-beta: Sleep sets McMini functions with relatively good performance using sleep sets, handling 10 threads in dining philosophers relatively easily. A clever observation about transitions in sleep sets allows us to only need to store around thread ids for sleep sets (and we don't have to store actual copies of transitions) McMini version 0.0.1 will include clock vectors and some other smaller optimizations that will improve its performance