Name
Abstract | ||
|---|---|---|
Well-defined memory consistency models are necessary for writing correct parallel software Developing and understanding formal specifications of hardware memory models is a challenge due to the subtle differences in allowed reorderings and different specification styles To facilitate exploration of memory model specifications, we have developed a technique for systematically comparing hardware memory models specified using both operational and axiomatic styles Given two specifications, our approach generates all possible multi-threaded programs up to a specified bound, and for each such program, checks if one of the models can lead to an observable behavior not possible in the other model When the models differs, the tool finds a minimal “litmus test” program that demonstrates the difference A number of optimizations reduce the number of programs that need to be examined Our prototype implementation has successfully compared both axiomatic and operational specifications of six different hardware memory models We describe two case studies: (1) development of a non-store atomic variant of an existing memory model, which illustrates the use of the tool while developing a new memory model, and (2) identification of a subtle specification mistake in a recently published axiomatic specification of TSO. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14295-6_26 | CAV |
Keywords | Field | DocType |
axiomatic specification,new memory model,different specification style,memory model specification,formal specification,axiomatic style,hardware memory model,existing memory model,different hardware memory model,generating litmus test,well-defined memory consistency model,memory model,software development | Programming language,Sequential consistency,Mistake,Computer science,Axiom,Litmus,Algorithm,Formal specification,Memory model,Consistency model,Parallel software | Conference |
Volume | ISSN | ISBN |
6174 | 0302-9743 | 3-642-14294-X |
Citations | PageRank | References |
23 | 0.82 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sela Mador-Haim | 1 | 174 | 6.87 |
| Rajeev Alur | 2 | 17253 | 1413.65 |
| Milo M. K. Martin | 3 | 2677 | 125.22 |