There is a term correctly synchronized in the JLS:
A program is correctly synchronized if and only if all sequentially consistent executions are free of data races.
If a program is correctly synchronized, then all executions of the program will appear to be sequentially consistent (§17.4.3).
Can this correctly synchronized be applied to something smaller than the whole program, like some collection class?
In other words, imagine that I want to create my custom concurrent collection class.
I want the code of my collection to never produce data races in any program which uses my collection.
Would it be enough to only check that every possible sequential execution has no data races in order to guarantee that non-sequential executions also cannot produce data races?
In my opinion, it's possible.
If the internal state of the collection is not accessible from the outside, then we can consider the corresponding to the state shared variables (that is what the JLS operates with) in isolation from the shared variables in the rest of the program.
This answer cites the proof for the whole program. But as I understand, the proofs for both Lemma 2 and Theorem 3 holds even if we add additional restriction that we only consider some shared variables.
Don't take my word for it and check the proofs yourself, but to me it seems like it works.
This holds as long as all the actions (reads and writes) on the selected shared variables are taken into consideration.
P.S. it's totally possible when simultaneously:
because:
A topological sort on the happens-before edges of the actions in an execution gives a total order consistent with program order and synchronization order.