/ klee Public
Multithread support v2 #240
Add this suggestion to a batch that can be applied as a single commit. This suggestion is invalid because no changes were made to the code. Suggestions cannot be applied while the pull request is closed. Suggestions cannot be applied while viewing a subset of changes. Only one suggestion per line can be applied in a batch. Add this suggestion to a batch that can be applied as a single commit. Applying suggestions on deleted lines is not supported. You must change the existing code in this line in order to create a valid suggestion. Outdated suggestions cannot be applied. This suggestion has been applied or marked resolved. Suggestions cannot be applied from pending reviews. Suggestions cannot be applied on multi-line comments. Suggestions cannot be applied while the pull request is queued to merge.
A review of the multithread support from Cloud9 presented in pull request: #211
This allows KLEE to execute C programs with pthread and semaphore calls and create new states based on thread scheduling.
In this version have cleaned and formatted the code, and cleaned up the git history (the main reason to open a new pull request).
The main points of the patch are:
1- added to the POSIX runtime a set of pthread calls for thread management, mutexes, condition variables and barriers. The pthread calls use 6 new klee_* special functions to define their behaviour: create, terminate, preempt, sleep, notify, retrieve thread id and retrieve current waiting list.
2- the scheduling is colaborative; the program under test must inform explicitly to KLEE that it can be preempted (using klee_thread_preempt). Some preemption points are hard coded in the pthread call definitions (mostly at the beginning and end of the call). If the user would like to have thread context changes in any other point must insert manually the call.
3- if a thread must wait for a specific action from other thread (mutex release, thread termination...), they are dsiable and put to sleep in a specific waiting list for the relevant event. The thread fulfilling the condition will wake-up one o more threads from the waiting list
4- ExecutionState now is composed by a collection of Threads, each one with its own program counter, incomingBBIndex, call stack. StackFrame struct was moved into the new Thread class. One of the Thread instances will correspond to the current active thread in the state, a set of shortcut methods allows to reference directly the Thread pc, callstack... from the ExecutionState instance.
6- Executor contains a new overloaded fork that clones the current state and add it to the execution pool. The schedule method of Executor is called when a thread is preempted and creates new states for alternative schedules, its behavior depends if the preemption is a real yield, a sleep or only a possible context change.
7- the Thread class keeps an account of each scheduling selection done in each preemption (even if the thread is not preempted at all). This shceduling history is added to the KTest instance; the ktest-tool has been also updated to show the scheduling.
8- new options:
-debug-sched-explored: after terminating an state prints the scheduling steps performed for that state
-debug-sched-history: print in each preemption from which thread to which thread is changing (with fork on schedule more that one new state can appear)
-fork-on-schedule: in each preemption create always new states (fork) for each alternative thread that could become the active one
-scheduler-preemption-bound: limits the number of possible preemptions (not yields) per thread to the given number
-no-scheduler-bound: make the option above unlimited (this increases enormously the number of generated tests)
9- note that the number of generated test cases will grow a lot, because each specific interleaving will reach a different ending state (to minimize this would require implement a partial order reduction algorithm).
10- the Executor::merge method will not merge two states that contains more than one thread, that should maintain the functionality in the sequential case, but I am not sure how that should work for a multithread case.
11- the Cloud9 license is conserved in the new files (directories indicated in LICENSE.TXT)
It would be nice if some (@ccadar, @ddunbar) can give it a try