Continuing with my previous message, a simplified version of my model is
at http://www.cs.uiuc.edu/~sadve/jmm.simpler.pdf. Here's what it does:
The model has only two conditions: One is for ensuring
not-out-of-thin-air values. This is currently the same as before,
although I am trying to simplify this too.
The second ensures that for any valid execution E of program P,
data-race-free parts of P appear SC. The main question has been how to
formalize "data-race-free parts of P." I do this by showing a
transformation of program P and execution E that allows focusing on
parts of the program or execution, and to consider the data-race-free or
SC properties of parts of the program or execution.
In more detail, here are the definitions (similar to P-R that I had
before):
For an execution E and program P, program P-M (read as "P minus M") is
defined as follows (some may find it more intuitive call this P|M; i.e.,
"P given M"):
If M is a memory read that returns value Val and updates register reg in
execution E: Then program P-M is the same as P except that instead of M,
it generates the assignment reg=Val for any execution with the same
backward slice for M as E.
If M is a memory write in execution E: Let {R1,...,Rn} be the set of
reads that return the value written by M in E. Then program P-M is the
same as P-R1-R2-...-Rn, with the write M additionally deleted whenever
the execution has the same backward slice for M as in E.
If M is a set of memory reads and writes {M1,...,Mn} in execution E:
Then Program P-M is P-M1-M2-...-Mn.
Execution E-M (E minus M) is analogous to P-M.
The memory model condition is (replaces the first three conditions in
pervious version):
For each subset of memory accesses, M, in execution E of program P, if
P-M is data-race-free, then E-M is an SC execution of P-M.
Comments?
Sarita
-----------------------------------------------------------------------
Sarita Adve
Associate Professor
University of Illinois at Urbana-Champaign Email: sadve@cs.uiuc.edu
Department of Computer Science Office: 3302 DCL
1304 West Springfield Avenue Phone: 217-333-8461
Urbana, IL 61801 Fax: 217-333-3501
WWW URL: http://www.cs.uiuc.edu/~sadve
-----------------------------------------------------------------------
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:41 EDT