Doug Lea wrote:
> Is getValue allowed by LC to return zero even in some purely single threaded
> context? The possibility of mirrored memory worlds ...
>
>
> > An example of architecture (Dr. Amaral from CAPSL had this idea) where
> > the example above could have V(r3)!=0 and V(r4)==0 both true would
> > provide more than one main memory. A system with several mirrors for its
> > main memory, where r3 would get w2 from one mirror and r4 would get w0
> > from another.
>
> ... has me both confused and worried.
>
> -Doug
The Gao-Sarkar Location Consistency model is presented in a 1998 memo
(www.capsl.udel.edu/LC.shtml). In that memo they present:
1. The LC model based partial-ordered multiset (pomset) of memory operations
and on a set of updating rules and ``visibility'' rules;
2. A protocol to implement the LC model in a multiprocessor with
caches and a main memory.
For some read operations, some values that are legal under the LC
model will never be returned by the cache protocol
For instance in this example:
T1 T2
w1: int v=0; w3: int v=0;
r1: if(v==0) r3: if(v==0);
w2: v=1; w4: v=2;
r2: return v; r4: return v;
According to Gao-Sarkar LC, r4 in T2 can read the value
written by (w1,w2,w3/w4) and r2 in Thread 2 can read the value written
by (w1/w2,w3,w4). In discussions with colleagues, I often find
that people have an easier time reasoning about existing machines.
Therefore sometimes I hear the following WRONG (according to LC)
theorem and proof:
Theorem: If r2 returns the value written by w4, then r4 must also return
the value written w4.
Proof: In order for r2 to ``see'' the value written by w4, T2 must
have written it to its cache and copied back to main memory
after w1 and/or w2 were written to the main memory. Therefore
the w4 in main memory would have killed w1/w2, and even if w4
is evicted from T2 cache, when it is reload to serve r4, the
only value available in main memory is the one written by w4.
What is WRONG with this reasoning??? We are deriving the set of legal
values to be returned by r4 from the POMSET based on the cache
protocol and NOT on the updating rules of LC.
In my opinion, we are often inclined to do so because there seems
to be no place for those older values (w1/w2) to be stored after the
value of w4 is ``passed'' from T2 to T1 through the main memory.
Below I create a story about a different system where LC could be used.
In this system we could easily accept that r2 returning w4 does not imply
that r4 cannot return w1/w2.
============ LC and Mirrowed Storage ==============================
1. Assume that I am running an internet-based company, lets call it T1.
- I want to mirrow my web page in many sites around the world.
2. I hire another company, lets call it ``Abstract Interpreter'' to do
the mirrowing of the page for me, and I sign a ``Location
Consistent Contract'' with the Abstract Interpreter in the following terms.
- Whenever I download my page from any server to my laptop I must
get the last version that I uploaded.
- The Abstract Interpreter can copy versions that I uploaded to
mirror sites at its own convenience.
- Whenever I release a version of the page, the Abstract
Interpreter must update all the mirror copies before confirming
that the release is complete.
- When one of my clients, lets call it T2, download a copy of my
page to their laptops, the Abstract Interpreter can deliver the
last released version, or any version that I uploaded after that
release.
- If a client acquires the page, it must receive the last released
version.
Observe that in this scenario I am maintaining single thread
consistency (whenever I download, I must receive that last version
that I uploaded).
However, if I and my clients only use upload/download
without _ever_ acquiring/releasing the page, there are places (the
mirror sites) where all the versions that I ever uploaded (the
legal values in the pomset in this case) can be stored.
This example is to illustrate that we must differenciate between the
legal values allowed in the model, and the values that could be
returned by existing machines.
Gao-Sarkar Location Consistency takes the position that if you want
synchronization, you must say so.
Cheers,
Nelson
/ Jose Nelson Amaral - amaral@capsl.udel.edu
\ / / http://www.capsl.udel.edu/~amaral
) / (
/ / \ Post-Doctoral Fellow: Elec. and Comp. Engineering
( / ) Univ. of Delaware, Newark, DE
\ O /
\ / Professor: EE - PUCRS - Porto Alegre - RS - Brazil
`----' Alumnus: ECE - The University of Texas at Austin
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:23 EDT