2

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.

Just Me
  • 413
  • 3
  • 9
  • FWIW, the quoted text is describing a recognizer, not a decider. – chrylis -cautiouslyoptimistic- Jan 01 '21 at 21:27
  • 1
    Also, I won't venture an opinion on this specific question, but this topic is wandering into the territory more usual on CS.SE, as it seems more about computation theory than a particular programming challenge. – chrylis -cautiouslyoptimistic- Jan 01 '21 at 21:31
  • Thanks @chrylis-cautiouslyoptimistic- for both your comments- I've edited my question accordingly. My intention was not to get into technical complexity-theory territory (which I know very little about anyway :-). Though from "The memory model ... *determines whether*..." I get the impression they're describing a decider. – Just Me Jan 01 '21 at 22:33
  • [here](https://stackoverflow.com/a/65016214/1059372) is an explanation I gave how a program correctness is build/proved using `PO`(program order), `SW` (syncronizes-with) and `HB` (happens before) rules according to the JLS. I _think_ this is what you are asking for, no? – Eugene Jan 03 '21 at 02:00
  • @Eugene I think the bit I'm referring to is checking something about possible JVM implementations, not possible programs. The question this algo addresses is roughly: "does this execution fit what the program says?" not "is this program well synchronized?" (which is what you seem to be referring to). In particular, the algo should apply also to programs which are *not* well-synchronized. It takes as an input an execution (not a program) and should spew out a sequence of subsets of actions meeting the causality requirements (not a proof of being well-sync'ed) – Just Me Jan 03 '21 at 07:43
  • hmm, how about [this, then](https://stackoverflow.com/questions/56273136/xxstresslcm-xxstressgcm-options-for-jvm)? I am still trying to understand what _exactly_ you mean, it might be just me because I am not a native english speaker and hard to grasp. – Eugene Jan 04 '21 at 20:42
  • @Eugene this is cool stuff (and potentially useful for me). But I don't think it's directly relevant here... basically I myself am trying to understand *exactly* what the authors of JLS mean (in the specific paragraph I pointed to), so you and I are both in the same boat. – Just Me Jan 04 '21 at 21:42

4 Answers4

3

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
snxsbwmr
  • 31
  • 1
  • 1
    I admit I did not expect for someone to answer, at all. A rather interesting paper! thank you for sharing – Eugene Jan 20 '21 at 21:09
2

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
Community
  • 1
  • 1
user19712778
  • 21
  • 1
1

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.

user19663120
  • 11
  • 1
0

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

user16992888
  • 1