WIXLIB

To be more concrete, here is an example of our tool in actionAn Example Our tool works to localize and repair concurrency bugsArray based liststruct list {int arr [ MAX SIZE ];size t open ;} gl ; By concurrency bugs, I mean those caused by some particular thread schedulerather than the sequential logic within a thread Consider this program where two threads modify a shared listvoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {Add operationint val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {Add operationint val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;thread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} The list is represented as an array with a integer value holding the next openposition Two threads are both concurrently adding items to the list The correctness specification states that after the threads execute, the listcontains both of their items. However, the add operation itself is unsynchronized: the update of the arrayand the update of the next available index is non-atomic As a result, the add operation of one thread may overwrite the result of theother thread causing the specification to be violated. First, the result of our localization procedure presents the programmer withminimal thread schedules leading to an assertion violation One such schedule is thread one’s add being overwritten by thread two An additional buggy schedule is the converse where thread two’s result isoverwritten by thread one4 By minimal thread schedule, I mean that our tool returns a schedule containingonly those statements which are involved in the bug rather than an completeschedule involving all statements in the program

To be more concrete, here is an example of our tool in actionAn Example Our tool works to localize and repair concurrency bugsArray based liststruct list {int arr [ MAX SIZE ];size t open ;} gl ; By concurrency bugs, I mean those caused by some particular thread schedulerather than the sequential logic within a thread Consider this program where two threads modify a shared listvoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {Add operationint val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {Add operationint val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;Specificationthread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} The list is represented as an array with a integer value holding the next openposition Two threads are both concurrently adding items to the list The correctness specification states that after the threads execute, the listcontains both of their items. However, the add operation itself is unsynchronized: the update of the arrayand the update of the next available index is non-atomic As a result, the add operation of one thread may overwrite the result of theother thread causing the specification to be violated. First, the result of our localization procedure presents the programmer withminimal thread schedules leading to an assertion violation One such schedule is thread one’s add being overwritten by thread two An additional buggy schedule is the converse where thread two’s result isoverwritten by thread one4 By minimal thread schedule, I mean that our tool returns a schedule containingonly those statements which are involved in the bug rather than an completeschedule involving all statements in the program

To be more concrete, here is an example of our tool in actionAn Example Our tool works to localize and repair concurrency bugsArray based liststruct list {int arr [ MAX SIZE ];size t open ;} gl ;Unsynchronized By concurrency bugs, I mean those caused by some particular thread schedulerather than the sequential logic within a thread Consider this program where two threads modify a shared listvoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {Add operationint val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {Add operationint val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;Specificationthread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} The list is represented as an array with a integer value holding the next openposition Two threads are both concurrently adding items to the list The correctness specification states that after the threads execute, the listcontains both of their items. However, the add operation itself is unsynchronized: the update of the arrayand the update of the next available index is non-atomic As a result, the add operation of one thread may overwrite the result of theother thread causing the specification to be violated. First, the result of our localization procedure presents the programmer withminimal thread schedules leading to an assertion violation One such schedule is thread one’s add being overwritten by thread two An additional buggy schedule is the converse where thread two’s result isoverwritten by thread one4 By minimal thread schedule, I mean that our tool returns a schedule containingonly those statements which are involved in the bug rather than an completeschedule involving all statements in the program

To be more concrete, here is an example of our tool in actionAn ExampleArray based liststruct list {int arr [ MAX SIZE ];size t open ;} gl ;Unsynchronizedvoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {Add operationint val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {Add operationint val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;Specificationthread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} Our tool works to localize and repair concurrency bugsThread oneThread Two By concurrency bugs, I mean those caused by some particular thread schedulerather than the sequential logic within a threads- arr[0] 1;s- arr[0] 2;open 1 Consider this program where two threads modify a shared list The list is represented as an array with a integer value holding the next openpositionopen 1 Two threads are both concurrently adding items to the list The correctness specification states that after the threads execute, the listcontains both of their items. However, the add operation itself is unsynchronized: the update of the arrayand the update of the next available index is non-atomic As a result, the add operation of one thread may overwrite the result of theother thread causing the specification to be violated. First, the result of our localization procedure presents the programmer withminimal thread schedules leading to an assertion violation One such schedule is thread one’s add being overwritten by thread two An additional buggy schedule is the converse where thread two’s result isoverwritten by thread one4 By minimal thread schedule, I mean that our tool returns a schedule containingonly those statements which are involved in the bug rather than an completeschedule involving all statements in the program

To be more concrete, here is an example of our tool in actionAn ExampleArray based liststruct list {int arr [ MAX SIZE ];size t open ;} gl ;Unsynchronizedvoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {Add operationint val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {Add operationint val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;Specificationthread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} Our tool works to localize and repair concurrency bugsThread oneThread Two By concurrency bugs, I mean those caused by some particular thread schedulerather than the sequential logic within a threads- arr[0] 1;s- arr[0] 2;open 1 Consider this program where two threads modify a shared list The list is represented as an array with a integer value holding the next openpositionopen 1 Two threads are both concurrently adding items to the list The correctness specification states that after the threads execute, the listcontains both of their items.Thread oneThread Two However, the add operation itself is unsynchronized: the update of the arrayand the update of the next available index is non-atomics- arr[0] 2; As a result, the add operation of one thread may overwrite the result of theother thread causing the specification to be violated.s- arr[0] 1;open 1 First, the result of our localization procedure presents the programmer withminimal thread schedules leading to an assertion violationopen 1 One such schedule is thread one’s add being overwritten by thread two An additional buggy schedule is the converse where thread two’s result isoverwritten by thread one4 By minimal thread schedule, I mean that our tool returns a schedule containingonly those statements which are involved in the bug rather than an completeschedule involving all statements in the program

An Example The second phase of our tool takes these fault localizations and usesthem to propose potential repairs to the userstruct list {int arr [ MAX SIZE ];size t open ;} gl ; One such repair is enforcing an ordering constraint between threadone’s add and thread two’svoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {int val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {int val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;thread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} Conversly, thread two could be constrainted to execute before threadone Each of these repairs is a happens-before constraints which, whenadded to the program, would prevent the assertion violation A single happens-before edge could be enforced using a signal–waitoperation across threads5

An Example The second phase of our tool takes these fault localizations and usesthem to propose potential repairs to the userstruct list {int arr [ MAX SIZE ];size t open ;} gl ; One such repair is enforcing an ordering constraint between threadone’s add and thread two’svoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {int val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {int val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;thread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} Conversly, thread two could be constrainted to execute before threadone Each of these repairs is a happens-before constraints which, whenadded to the program, would prevent the assertion violation A single happens-before edge could be enforced using a signal–waitoperation across threads5

An Example The second phase of our tool takes these fault localizations and usesthem to propose potential repairs to the userstruct list {int arr [ MAX SIZE ];size t open ;} gl ; One such repair is enforcing an ordering constraint between threadone’s add and thread two’svoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {int val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {int val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;thread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} Conversly, thread two could be constrainted to execute before threadone Each of these repairs is a happens-before constraints which, whenadded to the program, would prevent the assertion violation A single happens-before edge could be enforced using a signal–waitoperation across threads5

An Example For instance, here is one potential solution where thread one isguaranteed to execute before thread twocond var c1 ;void t1 main () {int val ;val 1;list add (& gl , val ) ;signal ( c1 ) ;return ;}void t2 main () {int val ;val 2;wait ( c1 ) ;list add (& gl , val ) ;return ;} The condition variable enforces the proposed happens-beforeconstraint In other words, the wait operation forces thread two to always addafter thread one However, exmaining this solution, while it prevents the error, it issomewhat unsatisfactory We lose the the extra potential parallelism by preventing thread twofrom running before thread one6

An Example For instance, here is one potential solution where thread one isguaranteed to execute before thread twocond var c1 ;void t1 main () {int val ;val 1;list add (& gl , val ) ;signal ( c1 ) ;return ;}void t2 main () {int val ;val 2;wait ( c1 ) ;list add (& gl , val ) ;return ;} The condition variable enforces the proposed happens-beforeconstraint In other words, the wait operation forces thread two to always addafter thread one However, exmaining this solution, while it prevents the error, it issomewhat unsatisfactory We lose the the extra potential parallelism by preventing thread twofrom running before thread one6

An Example However, examining the possible solutions we can see that there is athird possibilitystruct list {int arr [ MAX SIZE ];size t open ;} gl ; Notice that either thread one can execute before thread two orthread two can execute before thread onevoid list add ( list t *s , int i ) {s - arr [s - open ] i ;s - open 1;}void t1 main () {int val ;val 1;list add (& gl , val ) ;return ;}void t2 main () {int val ;val 2;list add (& gl , val ) ;return ;}int main () {thread t t1 , t2 ;thread create (& t1 , t1 main ) ;thread create (& t2 , t2 main ) ;thread join ( t1 ) ;thread join ( t2 ) ;assert ( list contains (& gl , 1)&& list contains (& gl , 2) ) ;return 0;} This either–or solution matches perfectly the design pattern of amutex lock7

An Example Here, we can see the automated fix of the third potential solution A mutex is inserted surrounding the add operations to enforce theeither–or constraintsmutex m ;void t1 main () {int val ;val 1;lock ( m ) ;list add (& gl , val ) ;unlock ( m ) ;return ;}void t2 main () {int val ;val 2;wait ( c1 ) ;lock ( m ) ;list add (& gl , val ) ;unlock ( m ) ;return ;} Here, we can see a fairly satisfactory repair The solution allows for additional parallelism compared to naivelyusing a signal–wait pair to enforce one of the ordering constraints To us, we found it interesting that our tool automatically lifted asequential list into a coarse-grained concurrent list8

Our Contributions In summary, here are our contributions We created a tool called ConcBugAssist ConcBugAssist is an extension of concurrent bounded modelchecking performing automated fault localization and repairI We formulate the problem of concurrent fault localization as asolution to the partial Max-SAT problemConcBugAssist We find potential repairs by solving the problem of a binate cover Both of these approaches are constraint based, which differs fromprior work in this area using mostly heuristics and pattern-matching. To validate our approach, we obtained some empirical data as wellhas some case studies showing the results of our tool The remainder of this talk will present these points in detail9

Our Contributions In summary, here are our contributions We created a tool called ConcBugAssist ConcBugAssist is an extension of concurrent bounded modelchecking performing automated fault localization and repairII We formulate the problem of concurrent fault localization as asolution to the partial Max-SAT problemConcBugAssistExtension to bounded model checking We find potential repairs by solving the problem of a binate cover Both of these approaches are constraint based, which differs fromprior work in this area using mostly heuristics and pattern-matching. To validate our approach, we obtained some empirical data as wellhas some case studies showing the results of our tool The remainder of this talk will present these points in detail9

Our Contributions In summary, here are our contributions We created a tool called ConcBugAssist ConcBugAssist is an extension of concurrent bounded modelchecking performing automated fault localization and repairIII We formulate the problem of concurrent fault localization as asolution to the partial Max-SAT problemConcBugAssistExtension to bounded model checkingConcurrent fault localization (partial Max-SAT) We find potential repairs by solving the problem of a binate cover Both of these approaches are constraint based, which differs fromprior work in this area using mostly heuristics and pattern-matching. To validate our approach, we obtained some empirical data as wellhas some case studies showing the results of our tool The remainder of this talk will present these points in detail9

Our Contributions In summary, here are our contributions We created a tool called ConcBugAssist ConcBugAssist is an extension of concurrent bounded modelchecking performing automated fault localization and repairIIII We formulate the problem of concurrent fault localization as asolution to the partial Max-SAT problemConcBugAssistExtension to bounded model checkingConcurrent fault localization (partial Max-SAT)Concurrent fault repair (binate covering) We find potential repairs by solving the problem of a binate cover Both of these approaches are constraint based, which differs fromprior work in this area using mostly heuristics and pattern-matching. To validate our approach, we obtained some empirical data as wellhas some case studies showing the results of our tool The remainder of this talk will present these points in detail9

Our Contributions In summary, here are our contributions We created a tool called ConcBugAssist ConcBugAssist is an extension of concurrent bounded modelcheck

ConcBugAssist: Constraint Solving for Diagnosis and Repair of Concurrency Bugs ISSTA 2015 Sepideh Khoshnood, Markus Kusano, Chao Wang Virgina Tech July 22, 2015 1 Thanks for the introduction . At this point, your beautiful creation decides to lash out with a runtime segmentation fault Its only now that the real hard work begins: you need to .