Question: The Java Language Specification provides [criteria](https://docs.oracle.com/javase/specs/jls/se15/html/jls-17.html#jls-17.4.8) 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](https://docs.oracle.com/javase/specs/jls/se15/html/jls-17.html#jls-17.4.8-A) 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: 
Yes, I think it's possible.

[The algorithm](https://docs.oracle.com/javase/specs/jls/se17/html/jls-17.html#jls-17.4.8) accepts [an execution](https://docs.oracle.com/javase/specs/jls/se17/html/jls-17.html#jls-17.4.6) 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](https://docs.oracle.com/javase/specs/jls/se17/html/jls-17.html#jls-17.4.8).  

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](https://github.com/javapathfinder/jpf-core/wiki) and [Lincheck](https://github.com/Kotlin/kotlinx-lincheck) might be capable of something like that.

P.S. [here](https://stackoverflow.com/a/66329398) is an example of how to apply [the algorithm](https://docs.oracle.com/javase/specs/jls/se17/html/jls-17.html#jls-17.4.8) to an execution.
You might want to look at research on JMM by Andreas Lochbihler at <http://www.andreas-lochbihler.de/>

Particularly in [his PhD Thesis](http://dx.doi.org/10.5445/KSP/1000028867) 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
> 
> 
>