Automatic synthesis of synchronisation primitives for concurrent programs (Record no. 358233)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 04029ntm a22003617a 4500 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | AT-ISTA |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20190813092902.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 170609s2016 a ||||| m||| 00| 0 eng d |
| 040 ## - CATALOGING SOURCE | |
| Transcribing agency | IST |
| 100 ## - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Tarrach, Thorsten |
| 9 (RLIN) | 3351 |
| 245 ## - TITLE STATEMENT | |
| Title | Automatic synthesis of synchronisation primitives for concurrent programs |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) | |
| Name of publisher, distributor, etc. | IST Austria |
| Date of publication, distribution, etc. | 2016 |
| 500 ## - GENERAL NOTE | |
| General note | Thesis |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Abstract |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Acknowledgments |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | About the Author |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Record of Publications |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Table of Contents |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | List of Tables |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | List of Figures |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | List of Abbreviations |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 1 Introduction |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 2 Formal framework and problem statement |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 3 Synthesis for an explicit specification |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 4 Regression-free synthesis |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 5 Synthesis of locks and other synchronisation primitives |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 6 Synthesis using an implicit specification |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 7 Conclusion |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Bibliography |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | List of Publications |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | In this thesis we present a computer-aided programming approach to concurrency. Our approach<br/>helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur<br/>when the program is executed using an aggressive preemptive scheduler, but not when using a<br/>non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t.<br/>a specification. We consider both user-provided explicit specifications in the form of assertion<br/>statements in the code as well as an implicit specification. The implicit specification is inferred<br/>from the non-preemptive behaviour. Let us consider sequences of calls that the program makes<br/>to an external interface. The implicit specification requires that any such sequence produced<br/>under a preemptive scheduler should be included in the set of sequences produced under a<br/>non-preemptive scheduler.<br/>We consider several semantics-preserving fixes that go beyond atomic sections typically<br/>explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers<br/>and wait-signal statements and last, but not least reorder independent statements. The latter<br/>may be useful if a thread is released to early, e.g., before some initialisation is completed. We<br/>guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted<br/>is optimal w.r.t. a given objective function.<br/>We dub our solution trace-based synchronisation synthesis and it is loosely based on<br/>counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a<br/>trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger<br/>the specification violation. Synchronisation may be placed immediately (greedy approach) or<br/>delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach<br/>we construct a set of global constraints over synchronisation placements. Each model of the<br/>global constraints set corresponds to a correctness-ensuring synchronisation placement. The<br/>placement that is optimal w.r.t. the given objective function is chosen as the synchronisation<br/>solution.<br/>We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver<br/>benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs.<br/>For the experiments with an explicit specification we added assertions that would detect the bugs<br/>in the experiments. Device drivers lend themselves to implicit specification, where the device and<br/>the operating system are the external interfaces. Our experiments demonstrate that our synthesis<br/>method is precise and efficient. We implemented objective functions for coarse-grained and<br/>fine-grained locking and observed that different synchronisation placements are produced for<br/>our experiments, favouring e.g. a minimal number of synchronisation operations or maximum<br/>concurrency. |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Source of classification or shelving scheme | Dewey Decimal Classification |
| Withdrawn status | Lost status | Source of classification or shelving scheme | Damaged status | Not for loan | Home library | Current library | Date acquired | Total Checkouts | Full call number | Barcode | Date last seen | Price effective from | Koha item type |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Not Lost | Dewey Decimal Classification | Library | Library | 09/06/2017 | Quiet Room | AT-ISTA#001350 | 15/09/2025 | 09/06/2017 | Book |