JavaMemoryModel: Possible weakening of Manson/Pugh model

From: Bill Pugh (
Date: Fri Aug 01 2003 - 15:17:05 EDT

Sarita suggested/proposed the following possible alternative to the
Manson/Pugh model as posted last night.

In the existing model, for each prescient action x, we compute a set
of justifications J and a set of prohibited executions P, and show
that for each E' in J-P, x is justified in E' (we also need to prove
that the set of prohibited executions is valid).

An alternative is to just show that there exists some E' in J such
that x is justified in E'.

This eliminates the need for prohibited executions, and can be shown
to be strictly weaker than the original Manson/Pugh model.

A result of this weakening is that the behaviors in causality test
cases 5 and 10 are allowed:

JavaMemoryModel mailing list -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT