topic.x86.group.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"x86" -ob topic.x86.group.bib groupbib.bib}}

@inproceedings{Ridge:2010:RPS:1884866.1884873,
  author = {Ridge, Tom},
  title = {A Rely-guarantee Proof System for x86-TSO},
  booktitle = {Proceedings of the Third International Conference on Verified Software: Theories, Tools, Experiments},
  conf = {VSTTE 2010},
  series = {VSTTE'10},
  year = {2010},
  isbn = {3-642-15056-X, 978-3-642-15056-2},
  location = {Edinburgh, UK},
  pages = {55--70},
  numpages = {16},
  opturl = {http://dl.acm.org/citation.cfm?id=1884866.1884873},
  acmid = {1884873},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  abstract = {Current multiprocessors provide weak or relaxed memory models. Existing program logics assume sequential consistency, and are therefore typically unsound for weak memory. We introduce a novel Rely-Guarantee style proof system for reasoning about x86 assembly programs running against the weak x86-TSO memory model. Interesting features of the logic include processor assertions which can refer to the local state of other processors (including their program counters), and a syntactic operation of closing an assertion under write buffer interference. We use the expressivity of the proof system to construct a new correctness proof for an x86-TSO version of Simpson's four slot algorithm. Mechanization in the Hol theorem prover provides a flexible tool to support semi-automated verification.},
  pdf = {http://www.cs.le.ac.uk/people/tr61/doc/ridge10vstte.pdf},
  topic = {x86}
}

@inproceedings{Owens:2010:RIC:1883978.1884011,
  author = {Owens, Scott},
  title = {Reasoning About the Implementation of Concurrency Abstractions on x86-TSO},
  conf = {ECOOP 2010},
  booktitle = {Proceedings of the 24th European Conference on Object-oriented Programming},
  series = {ECOOP'10},
  year = {2010},
  isbn = {3-642-14106-4, 978-3-642-14106-5},
  location = {Maribor, Slovenia},
  pages = {478--503},
  numpages = {26},
  opturl = {http://dl.acm.org/citation.cfm?id=1883978.1884011},
  acmid = {1884011},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  abstract = {
With the rise of multi-core processors, shared-memory concurrency has become a widespread feature of computation, from hardware, to operating systems, to programming languages such as C++ and Java. However, none of these provide sequentially consistent shared memory; instead they have relaxed memory models, which make concurrent programs even more challenging to understand. Programming language implementations run on hardware memory models, so VM and run-time system implementors must reason at both levels. Of particular interest are the low-level implementations of the abstractions that support language-level concurrency-especially because they invariably contain data races.

In this paper, we develop a novel principle for reasoning about assembly programs on our previous x86-TSO memory model, and we use it to analyze five concurrency abstraction implementations: two spinlocks (from Linux); a non-blocking write protocol; the double-checked locking idiom; and java.util.concurrent's Parker. Our principle, called triangular-race freedom, strengthens the usual data-race freedom style of reasoning.
},
  pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/ecoop10.pdf},
  topic = {x86},
  project = {http://www.cl.cam.ac.uk/~so294/ecoop2010/index.html}
}

@inproceedings{DBLP:conf/esop/SieczkowskiSBP15,
  author = {Filip Sieczkowski and
               Kasper Svendsen and
               Lars Birkedal and
               Jean Pichon{-}Pharabod},
  title = {A Separation Logic for Fictional Sequential Consistency},
  conf = {ESOP 2015},
  booktitle = {Programming Languages and Systems - 24th European Symposium on Programming,
               {ESOP} 2015, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015.
               Proceedings},
  pages = {736--761},
  year = {2015},
  optcrossref = {DBLP:conf/esop/2015},
  opturl = {http://dx.doi.org/10.1007/978-3-662-46669-8_30},
  doi = {10.1007/978-3-662-46669-8_30},
  timestamp = {Tue, 07 Apr 2015 15:18:50 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/SieczkowskiSBP15},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  abstract = {To improve performance, modern multiprocessors and programming languages typically implement relaxed memory models that
do not require all processors/threads to observe memory operations in
the same order. To relieve programmers from having to reason directly
about these relaxed behaviors, languages often provide efficient synchronization primitives and concurrent data structures with stronger high-level guarantees about memory reorderings. For instance, locks usually
ensure that when a thread acquires a lock, it can observe all memory
operations of the releasing thread, prior to the release. When used correctly, these synchronization primitives and data structures allow clients
to recover a fiction of a sequentially consistent memory model.
In this paper we propose a new proof system, iCAP-TSO, that captures
this fiction formally, for a language with a TSO memory model. The
logic supports reasoning about libraries that directly exploit the relaxed
memory model to achieve maximum efficiency. When these libraries provide sufficient guarantees, the logic hides the underlying complexity and
admits standard separation logic rules for reasoning about their more
high-level clients.},
  topic = {x86},
  pdf = {http://www.cl.cam.ac.uk/~pes20/group_papers/a_separation_logic_for_fictional_sequential_consistency.pdf}
}