Paper Info
Title
Tutorial: proving safety of parallel / multi-threaded programs.
Abstract
This tutorial will introduce the attendees to analysis and proof techniques for programs using parallelism and multi-threading. There are no specific prerequisites, but a familiarity with the notions of preconditions and postconditions, aliasing, race conditions, and deadlocks would be of value. The examples will be based on the threading and parallelism models of Java, Ada, and two new parallel languages, one called ParaSail [4] and another, inspired by the verifiable SPARK[1][2] subset of Ada, called Sparkel[3]. We will introduce the distinction between safety and liveness properties, and then focus primarily on techniques for the verification of safety properties, including the absence of race conditions and deadlocks. We will also discuss the issue of determinism vs. non-determinism in parallel and multi-threaded programs.
Year
DOI
Venue
2013
10.1145/2527269.2527285
HILT
Keywords
Field
DocType
safety property,liveness property,race condition,specific prerequisite,new parallel language,parallelism model,verifiable spark,multi-threaded program,proof technique,ada,java,multithreading,spark,parasail,deadlock detection,parallel programming
Multithreading,Programming language,Spark (mathematics),Computer science,Determinism,Deadlock,Deadlock prevention algorithms,Java,ParaSail,Liveness
Conference
Volume
Issue
ISSN
33
3
1094-3641
Citations 
PageRank 
References 
0
0.34
0
Authors
1
Name
Order
Citations
PageRank
S. Tucker Taft15014.12