Could "correctly synchronized" be applied to a class instead of the whole program?

Question

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?

Answer 1

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:

• actions on the selected shared variables (the ones which constitute the internal state of our collection) are sequentially consistent
• actions on the ignored shared variables contain data races

because:

1. it's always possible to find a total order of all actions in an execution, consistent with program order and synchronization order. From the citation:

   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.

2. actions on a shared variable are sequentially consistent if every read of the variable returns the latest (in this total order) write to the variable.
3. actions on a shared variable are non-sequentially-consistent if there is a read of the variable which returns a write to the variable that is not the latest (in this total order).
4. it's possible when both (2) and (3) are present in the execution

Answer 2

You need to ensure that there would be no race conditions is your concurrent custom collection.

I.e. multiple threads can access the same element simultaneously only if they are trying to read its value, that's fine. But if it's possible if one thread is trying to update the element while another is trying to retrieve its value, or multiple threads a trying to change the same element at the same time (overriding results produced by one-another), that's a problem. And it can be avoided by synchronizing the mutating code.

§17.4.5. Happens-before Order

When a program contains two conflicting accesses (§17.4.1) that are not ordered by a happens-before relationship, it is said to contain a data race.

§17.4.1. Shared Variables

Two accesses to (reads of or writes to) the same variable are said to be conflicting if at least one of the accesses is a write.

Here's a dummy example of the concurrent list which allows reading its value from multiple threads simultaneously, but if one of the threads is writing a value, all others would be blocked.

This can be achieved by using ReentrantReadWriteLock.

public class MyConcurrentArrayList<T> {
    private Object[] array;
    private int size;
    
    private final ReadWriteLock lock = new ReentrantReadWriteLock();
    private final Lock read = lock.readLock();
    private final Lock write = lock.readLock();
    
    // non-mutating operation
    @SuppressWarnings("unchecked")
    public T get(int i) {
        T result;
        
        read.lock(); // lock the read-lock, from that moment only non-mutating operations (guarded by the readLock) are allowed
        // access the element under the given index
        try {
            result = (T) array[i];
        } finally {
            read.unlock(); // release the read-lock
        }
        return result;
    }
    
    // mutating operation
    public void add(T item) {
        write.lock(); // lock the write-lock, none of the threads would be able to read or update the list until this lock is not released
        
        try {
            // check if the list needs to grow (omitted)

            array[size++] = item; // add a new element
        } finally {
            write.unlock(); // release the write-lock
        }
    }
}