is deciding the causality requirements of the java memory model tractable?

Question

The Java Language Specification provides criteria for determining whether a (well-formed) execution satisfies "the causality requirement for the Java memory model". Let's assume that the execution is finite. I'm trying to understand if there's a polynomial-time algorithm for proving or disproving that this is the case.

Really, I'm not looking for a detailed complexity-theory type analysis, the question can be paraphrased more loosely as: Do these causality requirements actually provide a practical definition that can be applied to executions of programs in practice - and if so, how?

Indeed, the wording of the blue box seems to imply that the authors did have a practical way of sifting through the space of chains of subsets of actions called for in the formal definition - which I do not understand:

The memory model takes as input a given execution, and a program, and determines whether that execution is a legal execution of the program. It does this by gradually building a set of "committed" actions that reflect which actions were executed by the program. Usually, the next action to be committed will reflect the next action that can be performed by a sequentially consistent execution. However, to reflect reads that need to see later writes, we allow some actions to be committed earlier than other actions that happen-before them...
Informally, we allow an action to be committed early if we know that the action can occur without assuming some data race occurs."

If someone can apply this sketch to a simple example - that would be very helpful too.

EDIT: it was pointed out that perhaps the authors had in mind a recognizer, not a decider. I'm good with either - the whole complexity angle is just a way to ask if / how this definition can be applied in practice.

Answer 1

I'm trying to understand if there's a polynomial-time algorithm for proving or disproving that this is the case.

The closest thing I can find is an algorithm in Verification of the Java Causality Feature by S. Polyakov and A. Schuster.
The algorithm is used on java program execution traces (i.e. after the program finishes).
Its complexity is polynomial if the trace provides a commitment order of Reads for each thread (which requires some support computer architecture support).

Indeed, the wording of the blue box seems to imply that the authors did have a practical way of sifting through the space of chains of subsets of actions called for in the formal definition - which I do not understand

The blue box contains a very condensed version of the JMM developers' reasoning behind the formal model of the JMM causality (which is located in the JLS right above the blue box).
If you want to see more detailed and easy-to-understand explanations, then I would recommend papers and articles by the creators of JMM: Jeremy Manson, William Pugh, Sarita Adve and Doug Lea.
For example these ones:

1. The Java Memory Model by J. Manson, W. Pugh and S. Adve, 2005.
   A nice short paper to start with.
2. The Java Memory Model by J. Manson, Ph.D. Thesis, 2004.
   This paper contains the most detailed explanations.
   The paper includes chapter about simulator, which is what was used for JMM verification.
3. Memory Models: A Case for Rethinking Parallel Languages and Hardware by S. Adve and H. Boehm, 2010.
   This is an overview paper:
   • it shows how the JMM compares to other memory models (both in hardware and in other programming languages)
   • it discusses what strong and weak sides of JMMs were discovered during the 5 years of its usage
   • it gives some potential directions of memory models development in the future

Answer 2

You might want to look at research on JMM by Andreas Lochbihler at http://www.andreas-lochbihler.de/

Particularly in his PhD Thesis you can find this:

In this thesis, I build a machine-checked model of Java concurrency called JinjaThreads for both Java source code and bytecode

Like its predecessor, JinjaThreads omits some sequential features from Java to remain tractable

Answer 3

Yes, I think it's possible.

The algorithm accepts an execution as input and outputs true if the execution is valid (i.e. satisfies the causality requirements), and false otherwise.
It works by committing step-by-step actions, executed by the program, according to the 9 rules.
If all the actions can be committed, then the execution is valid.

Personally, I would try to implement the algorithm backwards: it would start with the full execution, and then it would keep removing actions until none remains.
I'm not 100% sure, but it seems like at every step it's enough to test for deletion the last action in each thread.
This should be possible in polynomial time.

In practice the most frequent problem is probably: How to record an execution?
For example, for every read the execution should store the corresponding write action, which wrote the value returned by the read.
I don't think OpenJDK offers this functionality.
My guess would be that Java model checking tools like Java Pathfinder and Lincheck might be capable of something like that.

P.S. here is an example of how to apply the algorithm to an execution.

Answer 4

To add to the answer above, in 2008 another paper demonstrated a case when the algorithm proposed by Verification of the Java Causality Feature doesn't complete in polynomial time.

The paper is Verification of Causality Requirements in Java Memory Model is Undecidable by Matko Botin, Paola Glavan, and Davor Runje.
The conclusion in the paper:

the problem of verifying the JMM causality requirements for a finite execution of an arbitrary Java program is undecidable.

In short, the authors noticed that the original paper implicitly assumed that all intermediate executions used for justification are finite and polynomially bounded.
But in reality that is not always true, which was demonstrated by example.

The example can be simplified to the following.
The program:

Initially: y = 0, x = 0

Thread1  |  Thread2          
-----------------------------
y = x;   |  S;               
         |  x = 1;           

S is an arbitrary sequential program, which doesn't access x and y.
The execution that we need to verify produces result y == 1.
The reasoning:

• in order to get the result y == 1, x = 1; should be committed first
• x = 1; could be committed only if S doesn't execute infinitely.
  From the JLS:

  An execution may result in a thread being blocked indefinitely and the execution's not terminating. In such cases, the actions generated by the blocked thread must consist of all actions generated by that thread up to and including the action that caused the thread to be blocked, and no actions that would be generated by the thread after that action.

• determining if S executes infinitely is undecidable, because it's the halting problem