RSS 2.0

Personal Info:

Joe Send mail to the author(s) works on parallel libraries, infrastructure, and programming models in Microsoft's Developer Division.

Blogroll:
Other
News
 C|Net
 Kuro5hin
 The Register
Technology
 <?xmlhack?>
 Daily WTF
 DevX
 Hacknot
 Java Today
 Microsoft Top 10 Downloads
 MSDN
 MSDN: "Longhorn"
 MSDN: XML Developer Center
 Slashdot
 Techdirt
 theserverside.com
 W3C
 Web Pages That Suck
 XML Cover Pages
 XML Journal
 xml.com
Technology Blogs
 Aaron Skonnard [PluralSight]
 Adam Bosworth [Google]
 Andy Rich [MS/C++]
 Arpan Desai [MS/XML]
 BCL Team [MS]
 Bill Clementson [Lisp]
 Bill de hÓra
 Bruce Eckel [J]
 Bruce Tate [J]
 Casey Chestnut
 Cedric Beust [Google]
 Chris Anderson [MS/Avalon]
 Chris Lyon [MS]
 Christian Weyer
 Clemens Vasters [newtelligence]
 Craig Andera [PluralSight]
 Dan Sugalski [Parrot]
 Daniel Cazzulino
 Dave Chappel
 Dave Roberts [Lisp]
 Dave Thomas [PragProg]
 Dave Winer
 Dion Almaer [J]
 Don Demsak
 Doug Purdy [MS/Indigo]
 Drew Marsh
 Eric Gunnerson [MS]
 Eric Rudder [MS]
 Eric Sink
 Fritz Onion [PluaralSight]
 Gavin King [J/Hibernate]
 Grady Booch [IBM]
 Hervey Wilson [MS/Indigo]
 Hillel Cooperman [MS/Shell]
 Howard Lewis Ship [J/Apache]
 Ingo Rammer [PluralSight]
 James Gosling [J/Sun]
 James Strachan [J/Groovy]
 Jason Matusow [MS/OSS]
 Jeffrey Schlimmer [MS/Indigo]
 Joe Beda [Google]
 Joel Spoelsky
 Jon Udell
 Josh Ledgard [MS/Evang]
 Joshua Allen [MS]
 Lambda
 Larry Osterman [MS]
 Maoni Stephens [MS/CLR]
 Mark Fussell [MS/XML]
 Martin Fowler
 Martin Gudgin [MS/Indigo]
 Me
 Michael Howard [MS]
 Miguel de Icaza [Mono]
 Mike Clark
 Omri Gazitt [MS/Indigo]
 Pat Helland [MS/PAG]
 Pinku Surana
 Raymond Chen [MS]
 Rich Lander [MS/CLR]
 Rob Howard
 Rob Relyea [MS/Avalon]
 Robert Cringely
 S. Somasegar [MS/DevDiv]
 Sam Gentile
 Scoble [MS/Evang]
 Scott Guthrie [MS/WebNet]
 Scott Hanselman
 Sean McGrath [J]
 Simon Fell
 Stanley Lippman [MS/C++]
 Steve Maine
 Steve Swartz [MS/Indigo]
 Steve Vinoski
 Steven Clarke [MS/Usability]
 Stuart Halloway
 Ted Leung
 Ted Neward [DM]
 Tim Bray [Sun]
 Tim Ewald [Mindreef]
 Tim O'Reilly
 Werner Vogels [Amazon]
 Wintellect
 Yasser Shohoud [MS/Indigo]
Top 20
 Brad Abrams [MS/CLR]
 Chris Brumme [MS/CLR]
 Chris Sells [MS/Ultra]
 Cyrus Najmabadi [MS/C#]
 Dominic Cooney [MS/XAF]
 Don Box [MS/Ultra]
 Don Syme [MS/R]
 Guido van Rossum [Python]
 Herb Sutter [MS/C++]
 Ian Griffiths
 Jason Zander [MS/CLR]
 Jim Hugunin [MS/CLR]
 Joel Pobar [MS/CLR]
 Krzysztof Cwalina [MS/CLR]
 Patrick Logan
 Paul Graham
 Rico Mariani [MS/CLR]
 Rory Blyth [MS/DN]
 Sam Ruby
 Wesner Moise
VC/Business Blogs
 Ed Sim
 Fred Wilson
 Jonathan Schwartz [J/Sun]
 Lawrence Lessig [Stanford]
 Mark Cuban
 Michael Hyatt
 Pierre Omidyar
 Ross Mayfield
 VentureBlog
 Weekly Read
Wine, Food & Tea
 The Silk Road of Wine
 Vinography: a wine blog
 Wine Whys

Disclaimer:
The content of this site are my own personal opinions and do not represent my employer's view in anyway.

© 2008, Joe Duffy

 
 Sunday, July 20, 2008

Here's a slightly more formal approach to proving that the CLR MM is improperly implemented for the particular example I showed earlier.

As the Java MM folks have done, I will use a combination of happens-before and synchronizes-with relations, which allows order in a properly synchronized program to be describe as a "flat" sequence with total ordering among elements.  Assume < means synchronizes-with.  If a happens-before b, and a < b, then any writes in a are visible to any loads in b.  This relation is transitive: if a < b and b < c, then a < c.  Given this, we can take an observed set of results (the values held in memory locations), a hypothesized execution order (which we can infer from the observation), and validate it against the program order (as written in the source); we do this by taking the MM-specific synchronizes-with relation rules, and see if we can produce the observed output given our belief of the execution order.  If we find a contradiction (the execution order required to produce the output could not be produced given the program order and MM rules), either there is an alternative execution order we failed to guess, or we have found a violation of the memory model.

Single threaded programs are easy.  Multi threaded programs are hard.  We must manually "sequentialize" the program by constructing an interleaving of all executed program operations into a single flat sequence, and permute them as needed to produce the output in order to formulate a hypothesis of the execution order.  This is of course very difficult to do, so it only works with very small programs (like the one I will show below).

I will try to define the CLR 2.0 MM in terms of synchronizes-with, although I have to admit it’s going to be difficult to do off the top of my head:

  1. a < b, given a volatile load a that precedes any other memory operation b.  (Loads are acquire.)
  2. a < b, given any memory operation a that precedes any other store b.  (Stores are release.)
  3. a < b, given two separate memory operations a which precedes b that work with the same memory location.  (Data dependence.)
  4. a < b, given any memory operation a that precedes a full fence b.  (Cannot move after a fence.)
  5. a < b, given a full fence a that precedes some memory operation b.  (Cannot move before a fence.)
  6. a < b, given a lock acquire a that precedes some memory operation b.  (Lock acquires are acquire fences.)
  7. a < b, given a memory operation a that precedes a lock release b.  (Lock releases are release fences.)

Let’s take the disturbing example, assuming all loads and stores are volatile.

X = 1;              Y = 1;
R0 = X;             R2 = Y;
R1 = Y;             R3 = X;

Let’s hypothesize about execution order.

To produce an output in which R1 == R3 == 0, let us observe that it must be the case that X = 1 and Y = 1 must not happen first.  If one such instruction does occur first, then any possible outcome leads to R1 and/or R3 holding the value 1.  That is because of rule 3: if X = 1 happened first, then X = 1 < R3 = X, leading to R3 == 1 and similarly if Y = 1 happened first, then Y= 1 < R1 = Y, leading to R1 == 1.  So let us try to make X = 1 and Y = 1 not happen first.

Indeed, it is impossible for R0 = X or R2 = Y to happen first.  This is because of CLR MM rule 3: X = 1; R0 = X leads to data dependence, and thus X = 1 < R0 = X.  Similarly, Y = 1 < R2 = Y.  Dead end.  Let’s try the only other route.

The only remaining possibility to produce the output R1 == R3 == 0 is if R1 = Y or R3 = X occurs first.  Let us try to make R1 = Y occur first.  Ah-hah!  We cannot!  Given CLR MM rule 1, R0 = X < R1 = Y.  And because of transitivity, this necessarily implies that X = 1 < R1 = Y.  The same holds for the other thread’s instructions: Y = 1 < R3 = X.  The output R1 == R3 == 0 is therefore a contradiction and disallowed by the CLR MM.

Now, this is light years from a formal proof, but is the reasoning I’ve been using in my mind to explain why this new realization is fundamentally very disturbing and is explicitly not allowed by the CLR MM. Thankfully it seems the JIT team agrees and is willing to fix this for the next release. And, I'm still in search of an example of code that is broken by this problem ...

7/20/2008 1:14:14 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [1]

 Wednesday, July 16, 2008

The adjacent release/acquire problem is well known.  As an example, given the program:

P0          P1
==========  ==========
X = 1;      Y = 1;
R0 = Y;     R1 = X;

The outcome R0 == R1 == 0 is entirely legal.  This could happen because writes are delayed in processor store buffers; so before R0 = Y retires, the store X = 1 may have not even left the local processor P0; similarly, before R1 = X retires, the store Y = 1 may not have even left processor P1.  It is as if the program was written as follows:

P0          P1
==========  ==========
R0 = Y;     R1 = X;
X = 1;      Y = 1;

The standard way to fix this is to emit a full fence:

P0          P1
==========  ==========
X = 1;      Y = 1;
XCHG;       XCHG;
R0 = Y;     R1 = X;

But here is one that may be a little surprising:

P0          P1
==========  ==========
X = 1;      Y = 1;
R0 = X;     R2 = Y;
R1 = Y;     R3 = X;

Assuming X and Y are "volatile" to the compiler, is R1 == R3 == 0 a possible outcome in this program?

Based on the rules we provide for .NET's MM, and Intel's whitepaper, one could reasonably argue "no".  The reasoning goes as follows.  True data dependence prohibits R0 = X from moving before X = 1, and the no load/load reordering rule (e.g. Intel's Rule 2.1) prohibits R1 = Y from moving before R0 = X.  Thus, transitively, R1 = Y may not move before X = 1.  Similarly, true data dependence prohibits R2 = Y from moving before Y = 1, and the no load/load reordering rule prohibits R3 = X from moving before R2 = Y, and therefore R3 = X may not move before Y = 1.  Given this reasoning, the individual instruction streams cannot be reordered in place.  And therefore, no interleaving of them will yield R1 == R3 == 0, because either X = 1 or Y = 1 must happen first, and both R1 = Y and R3 = X must come later.  Hence at least one of R1 or R3 will observe a value of 1.

Sadly, this reasoning is incorrect.  Rule 2.4 in the Intel whitepaper states that "intra-processor forwarding is allowed."  They even have an innocent example in the paper, but it actually doesn't exhibit load/load reordering.  It does, however, illustrate that stores may be delayed for some time in a write buffer.  Perhaps surprisingly, such intra-processor forwarding of buffered stores is actually permitted to satisfy subsequent loads from that location by the same processor before the store has left the processor.  This can happen even if it means passing intermediate loads from different memory locations!  The result is that load/load reordering is effectively possible under some circumstances.  Loads still physically retire in order of course, but because they may be satisfied by pending writes that other processors cannot yet see, it is as if the original program were written as:

P0          P1
==========  ==========
R1 = Y;     R3 = X;
X = 1;      Y = 1;
R0 = X;     R2 = Y;

The fundamentally contradicts what most people believe about .NET's MM, and indeed, Intel's MM as specified in that whitepaper.  To be fair, the whitepaper actually does call this out, but in a roundabout and misleading fashion.  The text in Rule 2.1, which states that "no loads can be reordered with other loads", is far too strong.

Anytime a little hole in something as fundamental as MM axioms is uncovered, it is cause for concern.  So I found this discovery deeply disturbing.  Many abstractions and theorems are proved with the assumption that the MM is rock solid.  I know a lot of code I have written relies on such proofs.

That said, I've been racking my brain (and in fact was having nightmares about it last evening) trying to uncover a case where this is worse than the existing release/acquire reordering issue that I opened this post with.  Everything I come up with is saved at the last minute by rules 2.1 (for stores) and 2.5 "stores are transitively visible".  The basic problem is that a processor can get stuck seeing its own written value for some time, during which other processors cannot, but ultimately it doesn't seem to matter because the buffer will eventually be flushed.  Then any intermediary values that the destination may have held while that processor was stuck will have been overwritten anyway, so the outcome should be explainable (albeit racey).  I'm still thinking hard about this.

7/16/2008 7:43:00 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [21]

 Monday, June 23, 2008

I just submitted the final manuscript for Concurrent Programming on Windows to Addison-Wesley.

This marks the exciting transition from things happening on my timetable to things happening on AW’s timetable.

A lot has changed for me since I decided to write this book.  You might be surprised to hear that I actually signed the contract for it on November 29th, 2005.  That’s 2 years and 7 months ago.  It’s almost unbelievable that this book took so long to finish.  By comparison, my first one took just a little over a year.  The road has been a long one, full of personal ups and downs (I was, at the beginning, actually engaged to get married), but it’s no doubt been an exciting trip.

I’ve been at Microsoft the whole time.  At the outset, I was a PM on the CLR Team, hacking on software transactional memory and PLINQ as an evening activity.  Then I transitioned to doing it full time, but still as a PM.  Then I joined the Parallel Computing team as the dev for PLINQ.  Then I kicked off the whole Parallel Extensions effort (which is 20 members and growing strong), became the dev lead, and here I am today.  It’s pretty strange to say this, but without the book very little of that would have happened.  I can’t think of a better way to get entrenched in a technology, experience the breadth, and force yourself to learn every little intricate and often enlightening detail.  If you can afford the impact to mental health and personal relationships ;), it’s an activity I highly recommend to anybody wanting to master a technology...  not that one can actually master the concurrency beast, but y’know...

In retrospect, it should have taken a year.  Maybe next time.

The good news is that you will have the book in your hands soon.  (Well, if you decide to buy a copy, that is.)  If you manage to make it to my PDC 2008 pre-con session, I’m hoping we will have some copies available.  No promises, since I missed my final deadline by a couple weeks, but my fingers are crossed.

Oh yeah, and you can expect me to pick up blogging again now that I’ll have some free time.  Hmm, free time?  What will I do with myself!

Laissez les bon temps roulez!

6/23/2008 12:34:18 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [9]

 Friday, June 13, 2008

We had an interesting debate at a Parallel Extensions design meeting yesterday, where I tried to convince everybody that a full fence on SpinLock exit is not a requirement.  We currently offer an Exit(bool) overload that accepts a flushReleaseWrite argument.  This merely changes the lock release from

m_state = 0;

to

Interlocked.Exchange(ref m_state, 0);

The main purpose of this is to announce “availability” of the locks to other processors.  More specifically, it ensures that before the current processor is able to turn around and reacquire the lock in its own private cache, that other processors at least have the opportunity to see the write.  This is a fairness optimization, and avoiding the CAS on release halves the number of CAS operations necessary (which are expensive), so we would generally like to avoid superflous ones.  It turns out you could easily do this without our help.  Instead of

slock.Exit(true);

you could say

slock.Exit();
Thread.MemoryBarrier();

Most of the debate about whether the default Exit should use a fence centered around confusion over the strength of volatile vs. a full fence.  For example, the C# documentation for volatile is highly misleading (http://msdn.microsoft.com/en-us/library/x13ttww7(VS.71).aspx):

The volatile modifier is usually used for a field that is accessed by multiple threads without using the lock statement to serialize access. Using the volatile modifier ensures that one thread retrieves the most up-to-date value written by another thread.

The confusion is over the “ensures that one thread receives the most up-to-date value written by another thread” part.  Technically this is somewhat-accurate, but is worded in a very funny and misleading way.  To see why, let’s take a step back and consider what volatile actually means in the CLR’s memory model (MM) for a moment, to set context.  Note that I did my best to concisely summarize the MM here: http://www.bluebytesoftware.com/blog/2007/11/10/CLR20MemoryModel.aspx.

Volatile on loads means ACQUIRE, no more, no less.  (There are additional compiler optimization restrictions, of course, like not allowing hoisting outside of loops, but let’s focus on the MM aspects for now.)  The standard definition of ACQUIRE is that subsequent memory operations may not move before the ACQUIRE instruction; e.g. given { ld.acq X, ld Y }, the ld Y cannot occur before ld.acq X.  However, previous memory operations can certainly move after it; e.g. given { ld X, ld.acq Y }, the ld.acq Y can indeed occur before the ld X.  The only processor Microsoft .NET code currently runs on for which this actually occurs is IA64, but this is a notable area where CLR’s MM is weaker than most machines.  Next, all stores on .NET are RELEASE (regardless of volatile, i.e. volatile is a no-op in terms of jitted code).  The standard definition of RELEASE is that previous memory operations may not move after a RELEASE operation; e.g. given { st X, st.rel Y }, the st.rel Y cannot occur before st X.  However, subsequent memory operations can indeed move before it; e.g. given { st.rel X, ld Y }, the ld Y can move before st.rel X.  (I used a load since .NET stores are all release.)  Note that RELEASe is the opposite of ACQUIRE: you can think of an acquire as a one-way fence that prohibits passes downward, and a release as a one-way fence that prohibits passes upward.  A full fence prohibits both (lock acquire, XCHG, MB, etc).

Note one very interesting thing in this discussion: a release followed by an acquire, given the above rules, does not prohibit movement of the instructions with respect to one another!  Given { st.rel X, ld.acq Y }, even though they are both volatile (i.e. acquire and release), so long as X!=Y, it is perfectly legal for the ld.acq Y to move before st.rel X.  We aren’t limited to single instructions either, e.g. { st.rel X, ld.acq A, ld.acq B, ld.acq C }, all three loads (A, B, C) may indeed happen before the X.  This occurs with regularity in practice, on X86, X64, and IA64, because of store buffering.  It would just be too costly to hold up loads until a store has reached all processors.  Superscalar execution is meant to hide such latencies.

(As an aside, many people wonder about the difference between loads and stores of variables marked as volatile and calls to Thread.VolatileRead and Thread.VolatileWrite.  The difference is that the former APIs are implemented stronger than the jitted code: they achieve acquire/release semantics by emitting full fences on the right side.  The APIs are more expensive to call too, but at least allow you to decide on a callsite-by-callsite basis which individual loads and stores need the MM guarantees.)

I have to admit the store buffer problem is mostly theoretical.  It rarely comes up in practice.  That said, on a system which permits load reordering, imagine:

Initially: X = Y = 0

T0                       T1
X = 5; // st.rel         while (X == 0) ; // ld.acq
while (Y == 0) ; // ld   X = 0; // st.rel
A = X; // ld.acq         Y = 5; // st.rel

After execution, is it possible that A == 5?

If the read of Y is non-volatile on T0 (which would be bad because a compiler may hoist it out of the loop, but ignore compilers for a moment), then the fact that the subsequent read of X is volatile does not save us from a reordering leading to A == 5.  This is the { ld, ld.acq } case described earlier.  Why might this physically occur?  Well, it won’t happen on X86 and X64 because loads are not permitted to reorder.  However!!  IA64 permits non-acquire loads (non-volatile) to reorder, and so the A = X may actually be satisfied out of the write buffer before the store even leaves the processor.  It’s as though the program became:

T0                       T1
X = 5; // st.rel         while (X == 0) ; // ld.acq
A = X; // ld.acq         X = 0; // st.rel
while (Y == 0) ; // ld   Y = 5; // st.rel

Whoops!  This should make it apparent that this outcome is indeed a real possibility.  And clearly it may cause bugs.

Note 6/13/08: Eric pointed out privately that compilers need only respect the CLR MM, and can freely reorder loads.  Thus, this problem may actually arise on non-IA64 machines.  Of course he is entirely correct.  It was silly of me to overlook that.

All that said, let’s get back to the original concern about visibility of writes.  This issue doesn’t even really involve reordering.  Imagine one processor continuously executes a stream of lock acquires and releases, and that the stream goes on indefinitely (perhaps because it’s in a loop):

while (Interlocked.CompareExchange(ref m_state, 1, 0) != 0) ;
m_state = 0;
while (Interlocked.CompareExchange(ref m_state, 1, 0) != 0) ;
m_state = 0;

The Interlocked operation acquires the cache line in X mode.  After it executes, other processors will notice that the lock is taken.  But right away, the processor writes 0 to the line without a fence, and immediately goes on to execute another acquire.  It is highly likely that the line will be marked dirty in the processor’s cache by the time that it acquires it in X mode again, something that the cache coherency system makes very cheap.  In fact, the write of m_state = 0 probably hasn’t left the write buffer yet due to latency.

So before another processor can even see m_state as 0, the processor will have already gotten around to taking the lock again.  Even for volatile loads and stores, there is no MM guarantee that writes will leave the processor immediately; hence the documentaiton earlier is slightly confusing; yes, the processor doing a volatile read will see the “most recent” value, but that “most recent” value (a) may be satisfied out of the local write buffer, and (b) may simply not have the ability to observe writes that occurred in practice due to the above timeliness issue. 

6/13/2008 12:52:45 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [4]

 Thursday, June 05, 2008

We sat down last week with Charles from Channel9 to discuss the new CTP.  Both parts got posted today:

We focus on the new aspects of the stack, incl. the new scheduler and CDS, and also discuss what's changed in PLINQ and TPL.

If you have ideas for future videos, or any feedback/questions, you know where to send 'em.  joedu AT youknowwhere DOT com.

6/5/2008 5:14:47 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]

 

Recent Entries:

Search:

Browse by Date:
<July 2008>
SunMonTueWedThuFriSat
293012345
6789101112
13141516171819
20212223242526
272829303112
3456789

Browse by Category:

Notables:

Currently Up To:

Reading...

Listening...

Watching...