A unified formalization of four shared-memory models, IEEE Transactions on Parallel and Distributed Systems, vol.4, issue.6, pp.613-624, 1993. ,
DOI : 10.1109/71.242161
Reducing Opacity to Linearizability: A Sound and Complete Method. ArXiv e-prints, 1610. ,
A programming language perspective on transactional memory consistency, Proceedings of the 2013 ACM symposium on Principles of distributed computing, PODC '13, pp.309-318, 2013. ,
DOI : 10.1145/2484239.2484267
On Reducing Linearizability to State Reachability, LNCS, vol.9135, pp.95-107, 2015. ,
DOI : 10.1007/978-3-662-47666-6_8
Model checking of linearizability of concurrent list implementations, CAV. LNCS, pp.465-479, 2010. ,
Aspect-oriented linearizability proofs, Logical Methods in Computer Science, vol.11, issue.1, 2015. ,
DOI : 10.2168/LMCS-11(1:20)2015
Transactional Mutex Locks, Euro-Par, pp.2-13, 2010. ,
DOI : 10.1109/CGO.2009.30
URL : http://www.cs.rochester.edu/u/scott/papers/2009_TRANSACT_TML.pdf
NORec: streamlining STM by abolishing ownership records, pp.67-78, 2010. ,
Verifying Opacity of a Transactional Mutex Lock, FM. LNCS, pp.161-177, 2015. ,
DOI : 10.1007/978-3-319-19249-9_11
Formal Verification of a??Practical Lock-Free Queue Algorithm, FORTE. LNCS, pp.97-114, 2004. ,
DOI : 10.1006/inco.1995.1134
Towards formally specifying and verifying transactional memory. Formal Asp, Comput, vol.25, issue.5, pp.769-799, 2013. ,
DOI : 10.1007/s00165-012-0225-8
URL : http://research.sun.com/people/moir/pubs/Refine09-TM-correctness.pdf
Verifying Linearisability, ACM Computing Surveys, vol.48, issue.2, p.19, 2015. ,
DOI : 10.1007/978-3-642-29952-0_12
Model checking transactional memories, Distributed Computing, vol.54, issue.4, pp.129-145, 2010. ,
DOI : 10.1007/s00446-009-0092-6
On the correctness of transactional memory, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming , PPoPP '08, pp.175-184, 2008. ,
DOI : 10.1145/1345206.1345233
Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory, 2010. ,
Transactional Memory, Synthesis Lectures on Computer Architecture, 2010. ,
DOI : 10.1201/b11417-16
Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.463-492, 1990. ,
DOI : 10.1145/78969.78972
Communicating sequential processes, Communications of the ACM, vol.21, issue.8, pp.666-677, 1978. ,
DOI : 10.1145/359576.359585
The push/pull model of transactions, PLDI. PLDI '15, pp.186-195, 2015. ,
A Framework for Formally Verifying Software Transactional Memory Algorithms, pp.516-530, 2012. ,
DOI : 10.1007/978-3-642-32940-1_36
Putting opacity in its place, 2012. ,
Decomposing Opacity, LNCS, vol.8784, pp.391-405, 2014. ,
DOI : 10.1007/978-3-662-45174-8_27
Verifying Linearizability via Optimized Refinement Checking, IEEE Transactions on Software Engineering, vol.39, issue.7, pp.1018-1039, 2013. ,
DOI : 10.1109/TSE.2012.82
URL : http://research.microsoft.com/en-us/people/weic/tse13_linearizability.pdf
Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, ECOOP 2010, pp.478-503, 2010. ,
DOI : 10.1007/978-3-642-14107-2_23
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, ACM Transactions on Computational Logic, vol.15, issue.4, pp.1-3137, 2014. ,
DOI : 10.1145/1122971.1122992
PAT: Towards Flexible Verification under Fairness, CAV. LNCS, pp.709-714, 2009. ,
DOI : 10.1007/3-540-10843-2_22
URL : http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf
Modular fine-grained concurrency verification, 2007. ,