Loading...
Please wait, while we are loading the content...
Similar Documents
MemSAT: checking axiomatic specifications of memory models (2010)
| Content Provider | CiteSeerX |
|---|---|
| Author | Torlak, Emina Vaziri, Mandana Dol, Julian |
| Description | Memory models are hard to reason about due to their complexity, which stems from the need to strike a balance between ease-of-programming and allowing compiler and hardware optimizations. In this paper, we present an automated tool, MEMSAT, that helps in debugging and reasoning about memory models. Given an ax-iomatic specification of a memory model and a multi-threaded test program containing assertions, MEMSAT outputs a trace of the program in which both the assertions and the memory model ax-ioms are satisfied, if one can be found. The tool is fully automatic and is based on a SAT solver. If it cannot find a trace, it outputs a minimal subset of the memory model and program constraints that are unsatisfiable. We used MEMSAT to check several existing memory models against their published test cases, including the current Java Memory Model by Manson et al. and a revised version of it by Sevcik and Aspinall. We found subtle discrepancies be-tween what was expected and the actual results of test programs. In PLDI |
| File Format | |
| Language | English |
| Publisher Date | 2010-01-01 |
| Access Restriction | Open |
| Subject Keyword | Test Program Program Constraint Multi-threaded Test Program Containing Assertion Ax-iomatic Specification Subtle Discrepancy Revised Version Hardware Optimization Minimal Subset Test Case Automated Tool Sat Solver Memory Model Checking Axiomatic Specification Memory Model Ax-ioms Current Java Memory Model Actual Result |
| Content Type | Text |
| Resource Type | Article |
