Goal of this thesis is to build a basic toolset for verifying multi-threaded software and investigating the side effects of concurrent code in general.
This toolset consists of two main components: a simulator for replaying schedules generated by the solver.
A simple virtual machine for simulating random sequences of memory access by concurrent programs.
- 1 register (accumulator) + 1 hidden (mem - only used for compare and swap)
- 16 bit
- flat memory
- any number of threads > 1
- random schedule
Without a given seed, an infinite number of random memory access sequences will be generated. If the checker finds an error, the random seed used for that particular schedule will be stored and reported.
If a seed is given, the schedule of the resulting run will be reproduced.