menu

MemSAT: Checking Axiomatic Specifications of Memory Models

Torlak, Emina and Vaziri, Mandana and Dolby, Julian

PDF

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 axiomatic 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 axioms 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 between what was expected and the actual results of test programs.


@article{torlak+:sigplan10-memsat,
  address = {New York, NY, USA},
  author = {Torlak, Emina and Vaziri, Mandana and Dolby, Julian},
  date-added = {2020-11-15 23:36:57 -0800},
  date-modified = {2020-11-15 23:36:57 -0800},
  issn = {0362-1340},
  issue_date = {June 2010},
  journal = {SIGPLAN Not.},
  keywords = {memory models, bounded model checking, sat, axiomatic specifications},
  month = jun,
  number = {6},
  numpages = {10},
  pages = {341--350},
  publisher = {Association for Computing Machinery},
  title = {MemSAT: Checking Axiomatic Specifications of Memory Models},
  volume = {45},
  year = {2010},
  bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAkcGFwZXJzL3RvcmxhaytzaWdwbGFuMTAtbWVtc2F0LWEucGRmTxEBnAAAAAABnAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////HXRvcmxhaytzaWdwbGFuMTAtbWVtc2F0LWEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQADAAAKIGN1AAAAAAAAAAAAAAAAAAZwYXBlcnMAAgBDLzpVc2VyczpnYW1ibGluMjpzcmM6YnVpbGQtYmliOnBhcGVyczp0b3JsYWsrc2lncGxhbjEwLW1lbXNhdC1hLnBkZgAADgA8AB0AdABvAHIAbABhAGsAKwBzAGkAZwBwAGwAYQBuADEAMAAtAG0AZQBtAHMAYQB0AC0AYQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAQVVzZXJzL2dhbWJsaW4yL3NyYy9idWlsZC1iaWIvcGFwZXJzL3RvcmxhaytzaWdwbGFuMTAtbWVtc2F0LWEucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJABLAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAes=},
  bdsk-url-1 = {https://doi.org/10.1145/1809028.1806635}
}
Top