From 1927680d667f388a3c752a1f46ffe749bb7b499c Mon Sep 17 00:00:00 2001 From: Zeeshan Lakhani Date: Thu, 25 Sep 2014 13:46:07 -0400 Subject: [PATCH] add internal pwl paper on x86 semantics with note --- concurrency/README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/concurrency/README.md b/concurrency/README.md index 03af8d8..9136f16 100644 --- a/concurrency/README.md +++ b/concurrency/README.md @@ -7,3 +7,7 @@ * [Message Analysis for Concurrent Languages](http://user.it.uu.se/~kostis/Papers/escape.pdf) * [Finding Race Conditions in Erlang with QuickCheck and PULSE](http://publications.lib.chalmers.se/records/fulltext/125252/local_125252.pdf) + +* [The Semantics of x86-CC Multiprocessor Machine Code](http://www.cl.cam.ac.uk/~pes20/weakmemory/popl09.pdf) + + *Note: This contribution here is the focus on the rigorous semantics for x86 multiprocessor programs and an axiomatic definition of the memory model. Their definitions and proofs are backed by the [HOL](http://en.wikipedia.org/wiki/HOL_(proof_assistant))(Higher Order Logic) proof assistant.*