{"action":"created","issue":{"url":"https://api.github.com/repos/klee/klee/issues/211","labels_url":"https://api.github.com/repos/klee/klee/issues/211/labels{/name}","comments_url":"https://api.github.com/repos/klee/klee/issues/211/comments","events_url":"https://api.github.com/repos/klee/klee/issues/211/events","html_url":"https://github.com/klee/klee/pull/211","id":60633157,"number":211,"title":"Multithread support","user":{"login":"lmcarril","id":9567041,"avatar_url":"https://avatars.githubusercontent.com/u/9567041?v=3","gravatar_id":"","url":"https://api.github.com/users/lmcarril","html_url":"https://github.com/lmcarril","followers_url":"https://api.github.com/users/lmcarril/followers","following_url":"https://api.github.com/users/lmcarril/following{/other_user}","gists_url":"https://api.github.com/users/lmcarril/gists{/gist_id}","starred_url":"https://api.github.com/users/lmcarril/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lmcarril/subscriptions","organizations_url":"https://api.github.com/users/lmcarril/orgs","repos_url":"https://api.github.com/users/lmcarril/repos","events_url":"https://api.github.com/users/lmcarril/events{/privacy}","received_events_url":"https://api.github.com/users/lmcarril/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-03-11T09:48:22Z","updated_at":"2015-03-13T00:00:12Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/klee/klee/pulls/211","html_url":"https://github.com/klee/klee/pull/211","diff_url":"https://github.com/klee/klee/pull/211.diff","patch_url":"https://github.com/klee/klee/pull/211.patch"},"body":"This is a port of Cloud9 project multithread support to the current KLEE version. This allows KLEE to execute C programs with pthread and semaphore calls and create new states based on thread scheduling. \r\nThe followng is a list of the main points:\r\n\r\n1- 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.\r\n2- 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.\r\n3- 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\r\n4- 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. \r\n6- 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.\r\n7- 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.\r\n8- new options:\r\n    -debug-sched-explored: after terminating an state prints the scheduling steps performed for that state\r\n    -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)\r\n    -fork-on-schedule: in each preemption create always new states (fork) for each alternative thread that could become the active one\r\n    -scheduler-preemption-bound: limits the number of possible preemptions (not yields) per thread to the given number\r\n   -no-scheduler-bound: make the option above unlimited (this increases enormously the number of generated tests)\r\n9- 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).\r\n10- 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.\r\n11- It has benn tested only with LLVM 3.4, it includes three new tests and a couple of examples.\r\n12- the Cloud9 license is conserved in the new files (directories indicated in LICENSE.TXT)\r\n"},"comment":{"url":"https://api.github.com/repos/klee/klee/issues/comments/78704104","html_url":"https://github.com/klee/klee/pull/211#issuecomment-78704104","issue_url":"https://api.github.com/repos/klee/klee/issues/211","id":78704104,"user":{"login":"ccadar","id":5022313,"avatar_url":"https://avatars.githubusercontent.com/u/5022313?v=3","gravatar_id":"","url":"https://api.github.com/users/ccadar","html_url":"https://github.com/ccadar","followers_url":"https://api.github.com/users/ccadar/followers","following_url":"https://api.github.com/users/ccadar/following{/other_user}","gists_url":"https://api.github.com/users/ccadar/gists{/gist_id}","starred_url":"https://api.github.com/users/ccadar/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ccadar/subscriptions","organizations_url":"https://api.github.com/users/ccadar/orgs","repos_url":"https://api.github.com/users/ccadar/repos","events_url":"https://api.github.com/users/ccadar/events{/privacy}","received_events_url":"https://api.github.com/users/ccadar/received_events","type":"User","site_admin":false},"created_at":"2015-03-13T00:00:12Z","updated_at":"2015-03-13T00:00:12Z","body":"Hi @lmcarril , it's great to see that you have taken the initiative to port the Cloud9 pthread support into KLEE.  I haven't looked at the patch yet, but my main concern would be to make sure that the changes have a minimal effect on the symbolic execution of sequential programs. \r\n\r\n@ddunbar, you might like to take a look too. "}}