Automatic synthesis of synchronisation primitives for concurrent programs Dissertation Thesis

Author(s): Tarrach, Thorsten
Advisor(s): Henzinger, Thomas A
Committee Chair(s): Seiringer, Robert
Committee Member(s): Chatterjee, Krishnendu; Bloem, Roderick; Kovács, Laura; Cerný, Pavol
Title: Automatic synthesis of synchronisation primitives for concurrent programs
Affiliation IST Austria
Abstract: In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion statements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency.
Publication Title: IST Dissertation
Degree Granting Institution: IST Austria  
Degree: PhD
Degree Date: 2016-07-07
Start Page: 1
Total Pages: 151
Notes: I would like to thank all those people who helped me in the last four years to finish this thesis. First and foremost Thomas A. Henzinger whose advice proved invaluable to guide me along the way. Despite his responsibilities as a president he always has time for his students. Pavol Cerný and Arjun Radhakrishna helped me get a smooth start with my PhD by involving me into the project that would eventually make up this thesis. But before even starting my PhD at IST I visited Laura Kovács at TU Vienna who encouraged me to persue a PhD degree. I would also like to thank Roderick Bloem and Bettina Könighofer for the many interesting discussions and for inviting me to Graz. Thanks to the professors from my thesis committee for reviewing this thesis: Roderick Bloem, Krishnendu Chatterjee, Pavol Cerný, Thomas A. Henzinger and Laura Kovács. Further I am grateful to my collaborators Ashutosh Gupta, Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Roopsha Samanta for the fruitful collaborations we had. Without them I would not have been able to conduct this research. My office mates Przemysław Daca, Mirco Giacobbe, Andreas Pavlogiannis, Arjun Radhakrishna, Jakob Rueß and the usual coffee break crowd consisting of Sergiy Bogomolov, Ventsislav Chonev, Rasmus Ibsen-Jensen, Bernhard Kragl, Petr Novotný, Jan Otop and Roopsha Samanta made my time at IST a much more pleasent experience
Open access: no
IST Austria Authors
Related IST Austria Work