1. linux kernel mailing list, thread
"spin_unlock optimization (i386)",
119 messages, nov. 20–Dec. 7, 1999,
http://www.gossamer-threads.com/
lists/engine?post=105365;list=linux.
Accessed 2009/11/18.
2. The SPARC Architecture Manual, V.
8. sPARC International, Inc., 1992.
Revision sAV080sI9308. http://www.
sparc.org/standards/V8.pdf.
3. AMD64 Architecture Programmer’s
Manual ( 3 vols). Advanced Micro
Devices, sept. 2007. rev. 3. 14.
4. Intel 64 architecture memory
ordering white paper, 2007. Intel
Corporation. sKu 318147-001.
5. Intel 64 and IA- 32 Architectures
Software Developer’s Manual ( 5 vols).
Intel Corporation, Mar. 2010. rev. 34.
6. Adve, s. Gharachorloo, K. shared
memory consistency models: A
tutorial. IEEE Comput. 29, 12 (Dec.
1996), 66–76.
7. Adve, s.V., boehm, h.-j. Memory
models: A case for rethinking parallel
languages and hardware. C. ACM. To
appear.
8. Adve, s.V., hill, M.D. A unified
formalization of four shared-memory
models. IEEE Trans. Parallel Distrib.
Syst. 4, 6 (1993), 613–624.
9. Ahamad, M., neiger, G., burns, j.,
Kohli, P., hutto, P. Causal memory:
Definitions, implementation, and
programming. Distrib. Comput. 9, 1
(1995), 37–49.
10. Aspinall, D., Ševčík j. Formalising
java’s data race free guarantee. In
Proc. TPHOLs, LNCS 4732 (2007),
22–37.
11. boehm, h.-j.. Adve, s. Foundations of
the C++ concurrency memory model.
References
In Proceedings of PLDI (2008).
12. boudol, G., Petri, G. Relaxed memory
models: An operational approach.
In Proceedings of POPL, 2009.
13. burckhardt, s., Musuvathi, M.
effective program verification for
relaxed memory models. Technical
Report MsR-TR-2008-12, Microsoft
Research, 2008. Conference version
in Proceedings of CAV, LNCS 5123
(2008).
14. burckhardt, s., Musuvathi, M., singh,
V. Verifying compiler transformations
for concurrent programs, jan. 2009.
Technical report MsR-TR-2008-171.
15. Dice, D. java memory model
concerns on Intel and AMD systems.
http://blogs.sun.com/dave/entry/
java_memory_model_concerns_on,
jan. 2008.
16. Friedman, R. Consistency conditions
for distributed shared memories.
Israel Institute of Technologie, 1994.
17. Gharachorloo, K. Memory consistency
models for shared-memory
multiprocessors. WRL Res. Rep. 95, 9
(1995).
18. hangal, s., Vahia, D., Manovit, C.,
lu, j.-y.j., narayanan, s. Tsotool:
A program for verifying memory
systems using the memory
consistency model. In Proceedings of
ISCA (2004), 114–123.
19. higham, l., Kawash, j., Verwaal, n.
Weak memory consistency models
part I: Definitions and comparisons.
Technical Report98/612/03,
Department of Computer science,
The University of Calgary, January,
1998. Full version of a paper in PDCs
1997.
20. The hol 4 system. http://hol.
sourceforge.net/.
21. lamport, l. how to make a
multiprocessor computer that
correctly executes multiprocess
programs. IEEE Trans. Comput. C- 28,
9 (1979), 690–691.
22. loewenstein, P.n., Chaudhry, s.,
Cypher, R., Manovit, C. Multiprocessor
memory model verification. In
Proceedings of AFM (Automated
Formal Methods) (Aug. 2006). FloC
workshop. http://fm.csl.sri.com/
AFM06/.
23. luchango, V.M. Memory consistency
models for high-performance
distributed computing. PhD thesis,
MIT, 2001.
24. Manson, j., Pugh, W., Adve, s. The
java memory model. In Proceedings
of POPL (2005).
25. Milner, R. Communication and
Concurrency. Prentice hall
International, 1989.
26. owens, s. Reasoning about the
implementation of concurrency
abstractions on x86-Tso. In
Proceedings of ECOOP (2010).
To appear.
27. owens, s., sarkar, s., sewell, P. A
better x86 memory model: x86-Tso.
In Proceedings of TPHOLs, LNCS
5674 (2009), 391–407. Full version as
Technical Report uCAM-Cl-TR-745,
© 2010 ACM 0001-0782/10/0700 $10.00
Peter Sewell ( http://www.cl.cam.
ac.uk/~pes20), university of Cambridge.
Susmit Sarkar ( http://www.cl.cam.
ac.uk/~ss726), university of Cambridge.
Scott Owens ( http://www.cl.cam.
ac.uk/~so294), university of Cambridge.
univ. of Cambridge.
28. Park, s., Dill, D.l. An executable
specification and verifier for relaxed
memory order. IEEE Trans. Comput.
48, 2 (1999), 227–235.
29. Roy, A., Zeisset, s., Fleckenstein, C.j.,
huang, j.C. Fast and generalized
polynomial time memory consistency
verification. In CAV (2006), 503–516.
30. saraswat, V., jagadeesan, R.,
Michael, M., von Praun, C. A theory of
memory models. In Proceedings of
PPoPP (2007).
31. sarkar, s., sewell, P., Zappa nardelli,
F., owens, s., Ridge, T., braibant, T.,
Myreen, M., Alglave, j. The semantics
of x86-CC multiprocessor machine
code. In Proceedings of POPL 2009
(jan. 2009).
32. sindhu, P.s., Frailong, j.-M., Cekleov,
M. Formal specification of memory
models. In Scalable Shared Memory
Multiprocessors, Kluwer, 1991,
25–42.
33. Ševcík, j., Aspinall, D. on validity of
program transformations in the java
memory model. In ECOOP (2008),
27–51.
ˇ
Francesco Zappa nardelli (http://www.
moscova.inria.fr/~zappa), InRIA.
Magnus O. Myreen ( http://www.cl.cam.
ac.uk/~mom22), university of Cambridge.
Announcing ACM’s Newly Improved
Career & Job Center!
Are you looking for your next IT job? Do you need Career Advice?
Visit ACM’s newly enhanced career resource at:
http://www.acm.org/careercenter
◆ ◆ ◆ ◆ ◆
The ACM Career & Job Center offers ACM members a host of benefits including:
➜ A highly targeted focus on job opportunities in the computing industry
➜ Access to hundreds of corporate job postings
➜ Resume posting keeping you connected to the employment market while letting you maintain full
control over your confidential information
➜ An advanced Job Alert system that notifies you of new opportunities matching your criteria
➜ Career coaching and guidance from trained experts dedicated to your success
➜ A content library of the best career articles complied from hundreds of sources, and much more!
The ACM Career & Job Center is the perfect place to
begin searching for your next employment opportunity!
