Confused by jcstress test on ReentrantReadWriteLock#tryLock failing

Question

I am trying to get to grips with JCStress. To ensure I understand it, I decided to write some simple tests for something that I know must be correct: java.util.concurrent.locks.ReentrantReadWriteLock.

I wrote some very simple tests to check lock mode compatibility. Unfortunately two of the stress tests are failing:

1. X_S:

   true, true        32,768     FORBIDDEN  No default case provided, assume FORBIDDEN
   

2. X_X:

   true, true        32,767     FORBIDDEN  No default case provided, assume FORBIDDEN
   

It seems to me that one thread should not be able to hold the read lock, whilst another thread also holds the write lock. Likewise, it should be impossible for two threads to simultaneously hold the write lock.

I realise that the problem is likely not with ReentrantReadWriteLock. I figure that I am probably making some stupid mistake in my jcstress tests with regards to the JMM and reading the state of the locks.

Unfortunately, I am not able to spot the problem. Can someone please help me understand the (stupid?) mistake that I have made?

import org.openjdk.jcstress.annotations.*;
import org.openjdk.jcstress.infra.results.ZZ_Result;

import java.util.concurrent.locks.ReentrantReadWriteLock;

/*
 * |-----------------|
 * |  COMPATIBILITY  |
 * |-----------------|
 * |     | S   | X   |
 * |-----------------|
 * | S   | YES | NO  |
 * | X   | NO  | NO  |
 * |-----------------|
 */
public class ReentrantReadWriteLockBooleanCompatibilityTest {

    @State
    public static class S {
        public final ReentrantReadWriteLock lock = new ReentrantReadWriteLock();

        public boolean shared() {
            return lock.readLock().tryLock();
        }

        public boolean exclusive() {
            return lock.writeLock().tryLock();
        }
    }

    @JCStressTest
    @Outcome(id = "true, true", expect = Expect.ACCEPTABLE, desc = "T1 and T2 are both acquired S")
    public static class S_S {
        @Actor
        public void actor1(S s, ZZ_Result r) { r.r1 = s.shared(); }
        @Actor
        public void actor2(S s, ZZ_Result r) { r.r2 = s.shared(); }
    }

    @JCStressTest
    @Outcome(id = "true, false", expect = Expect.ACCEPTABLE, desc = "T1 acquired S, and T2 could not acquire X")
    @Outcome(id = "false, true", expect = Expect.ACCEPTABLE, desc = "T2 acquired X, and T1 could not acquire S")
    public static class S_X {
        @Actor
        public void actor1(S s, ZZ_Result r) { r.r1 = s.shared(); }
        @Actor
        public void actor2(S s, ZZ_Result r) { r.r2 = s.exclusive(); }
    }

    @JCStressTest
    @Outcome(id = "true, false", expect = Expect.ACCEPTABLE, desc = "T1 acquired X, and T2 could not acquire S")
    @Outcome(id = "false, true", expect = Expect.ACCEPTABLE, desc = "T2 acquired S and T1 could not acquire X")
    public static class X_S {
        @Actor
        public void actor1(S s, ZZ_Result r) { r.r1 = s.exclusive(); }
        @Actor
        public void actor2(S s, ZZ_Result r) { r.r2 = s.shared(); }
    }

    @JCStressTest
    @Outcome(id = "true, false", expect = Expect.ACCEPTABLE, desc = "T1 acquired X, and T2 could not acquire X")
    @Outcome(id = "false, true", expect = Expect.ACCEPTABLE, desc = "T2 acquired X and T1 could not acquire X")
    public static class X_X {
        @Actor
        public void actor1(S s, ZZ_Result r) { r.r1 = s.exclusive(); }
        @Actor
        public void actor2(S s, ZZ_Result r) { r.r2 = s.exclusive(); }
    }
}

I did try asking about this on the jcstress-dev but never received a response - http://mail.openjdk.java.net/pipermail/jcstress-dev/2018-August/000346.html. Apologies for cross-posting, but I need help with this, and so I am reposting to StackOverflow in the hope of getting attention from a larger audience.

Answer 1

Your tests pass when run against jcstress 0.3. In version 0.4 the behaviour changed to include the results of the sanity checks that are run on startup (see this commit against the bug jcstress omits samples gathered during sanity checks).

Some of the sanity checks run in a single thread, and your test doesn't handle the case where both actors are called by the same thread; you're testing a reentrant lock, so the read lock will pass if the write lock is already held.

This is arguably a bug in jcstress, as the documentation on @Actor says the invariants are:

• Each method is called only by one particular thread.
• Each method is called exactly once per State instance.

While the documentation is not that clearly worded, the generated source makes it clear that the intention is to run each actor in its own thread.

One way to work around it would be to allow the single threaded case to pass:

@State
public static class S {
    public final ReentrantReadWriteLock lock = new ReentrantReadWriteLock();

    public boolean shared() {
        return lock.readLock().tryLock();
    }

    public boolean exclusive() {
        return lock.writeLock().tryLock();
    }

    public boolean locked() {
        return lock.isWriteLockedByCurrentThread();
    }
}

@JCStressTest
@Outcome(id = "true, false, false", expect = Expect.ACCEPTABLE, desc = "T1 acquired X, and T2 could not acquire S")
@Outcome(id = "false, false, true", expect = Expect.ACCEPTABLE, desc = "T2 acquired S and T1 could not acquire X")
@Outcome(id = "true, true, true", expect = Expect.ACCEPTABLE, desc = "T1 acquired X and then acquired S")
public static class X_S {
    @Actor
    public void actor1(S s, ZZZ_Result r) {
        r.r1 = s.exclusive();
    }
    @Actor
    public void actor2(S s, ZZZ_Result r) {
        r.r2 = s.locked();
        r.r3 = s.shared();
    }
}

Or check for the single threaded case and mark it as "interesting" instead of accepted:

@State
public static class S {
    public final ReentrantReadWriteLock lock = new ReentrantReadWriteLock();
    public AtomicReference<Thread> firstThread = new AtomicReference<>();

    public boolean shared() {
        firstThread.compareAndSet(null, Thread.currentThread());
        return lock.readLock().tryLock();
    }

    public boolean exclusive() {
        firstThread.compareAndSet(null, Thread.currentThread());
        return lock.writeLock().tryLock();
    }

    public boolean sameThread() {
        return Thread.currentThread().equals(firstThread.get());
    }

    public boolean locked() {
        return lock.isWriteLockedByCurrentThread();
    }
}

@JCStressTest
@Outcome(id = "false, true, false, false", expect = Expect.ACCEPTABLE, desc = "T1 acquired X, and T2 could not acquire X")
@Outcome(id = "false, false, false, true", expect = Expect.ACCEPTABLE, desc = "T2 acquired X and T1 could not acquire X")
@Outcome(id = "false, true, true, true", expect = Expect.ACCEPTABLE_INTERESTING, desc = "Both actors ran in the same thread!")
@Outcome(id = "true, true, false, true", expect = Expect.ACCEPTABLE_INTERESTING, desc = "Both actors ran in the same thread!")
public static class X_X {
    @Actor
    public void actor1(S s, ZZZZ_Result r) {
        r.r1 = s.sameThread();
        r.r2 = s.exclusive();
    }
    @Actor
    public void actor2(S s, ZZZZ_Result r) {
        r.r3 = s.sameThread();
        r.r4 = s.exclusive();
    }
}

As you noted in the comments, the final @Outcome in the above test never happens. This is because the single threaded sanity check doesn't shuffle the actors before running them (see the method sanityCheck_Footprints on your generated test class).