Automatic synthesis of synchronisation primitives for concurrent programs (Record no. 358233)

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
Holdings
Withdrawn status Lost status Source of classification or shelving scheme Damaged status Not for loan Permanent Location Current Location Date acquired Barcode Date last seen Price effective from Koha item type
  Not Lost       Library Library 2017-06-09 AT-ISTA#001350 2018-11-06 2017-06-09 Book

Powered by Koha