Abstract
The growing complexity of hardware optimizations employed
by multiprocessors leads to subtle distinctions among allowed and dis-
allowed behaviors, posing challenges in specifying their memory models
formally and accurately, and in understanding and analyzing the behavior of concurrent software. This complexity is particularly evident in the
IBM Power Architecture , for which a faithful specification was published only in 2011 using an operational style. In this paper we present
an equivalent axiomatic specification, which is more abstract and concise. Although not officially sanctioned by the vendor, our results indicate
that this axiomatic specification provides a reasonable basis for reasoning
about current IBM POWER multiprocessors. We establish the equivalence of the axiomatic and operational specifications using both manual
proof and extensive testing. To demonstrate that the constraint-based
style of axiomatic specification is more amenable to computer-aided verification, we develop a SAT-based tool for evaluating possible outcomes
of multi-threaded test programs, and we show that this tool is significantly more efficient than a tool based on an operational specification.
by multiprocessors leads to subtle distinctions among allowed and dis-
allowed behaviors, posing challenges in specifying their memory models
formally and accurately, and in understanding and analyzing the behavior of concurrent software. This complexity is particularly evident in the
IBM Power Architecture , for which a faithful specification was published only in 2011 using an operational style. In this paper we present
an equivalent axiomatic specification, which is more abstract and concise. Although not officially sanctioned by the vendor, our results indicate
that this axiomatic specification provides a reasonable basis for reasoning
about current IBM POWER multiprocessors. We establish the equivalence of the axiomatic and operational specifications using both manual
proof and extensive testing. To demonstrate that the constraint-based
style of axiomatic specification is more amenable to computer-aided verification, we develop a SAT-based tool for evaluating possible outcomes
of multi-threaded test programs, and we show that this tool is significantly more efficient than a tool based on an operational specification.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 24th International Conference on Computer Aided Verification |
| Editors | P Madhusudan, Sanjit Seshia |
| Publisher | Springer-Verlag |
| Pages | 495 |
| Number of pages | 512 |
| ISBN (Print) | 978-3-642-31423-0 |
| DOIs | |
| Publication status | Published - Jul 2012 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 7358 |