At 04:04 PM 15/04/2004 +1000, David Holmes wrote:
>What I'm getting stuck on is a set of rules for reasoning about whether
>certain reorderings are allowed, such that I can reason about lock-free
>algorithm using volatiles.
I think this way lies madness. The model simply isn't defined in terms of
permitted or non-permitted reorderings.
If you want to make some assertion in your lock free algorithm you need to
find a combination of happens-before and synchronization orderings that
supports it. If you can't find one, (and it in fact doesn't exist) then
your assertion is not sustainable. While looking, you'll likely realise
where a happens-before edge or synchronization ordering would have helped.
Then you can add reads and writes to achieve it.
Look back at my two recent postings under the subject "Re: JavaMemoryModel:
Use-case for strong volatile" and my discussion of the optimistic reader
pattern. There's nothing in there about the order in which things actually
happen or permitted reorderings. It's just reasoning about happens-before
and synchronization orderings specified by the model.
From Bill's short response, it seems I arrived at the right answer even
though it wasn't original.
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:04 EDT