Invariants with multiple threads

[nhatminhle]

From [email protected] on May 20, 2011 08:22:38

What steps will reproduce the problem? 1. I've noticed that in some cases my invariants are failing, and yet in a debugger the conditions seem to be satisfied. The class itself is updated by multiple threads simultaneously, protected by synchronized methods. However, one explanation for the error I'm seeing is that the @invariant calculation is not thread-safe, and so sometimes fails due to race conditions. What version of the product are you using? On what operating system? r120 Please provide any additional information below. These last invariants sometimes trigger when running with multiple threads.

@Invariant({
        "dict != null",
        "dict.size() > 0",
        "lastSSR == null || dict.getSequence(lastContig).getSequenceIndex() == lastIndex",
        "lastSSR == null || dict.getSequence(lastContig).getSequenceName() == lastContig",
        "lastSSR == null || dict.getSequence(lastContig) == lastSSR"})
private final class MasterSequenceDictionary {
    final private SAMSequenceDictionary dict;

    // cache
    SAMSequenceRecord lastSSR = null;
    String lastContig = "";
    int lastIndex = -1;

    @Requires({"dict != null", "dict.size() > 0"})
    public MasterSequenceDictionary(SAMSequenceDictionary dict) {
        this.dict = dict;
    }

    @Ensures("result > 0")
    public final int getNSequences() {
        return dict.size();
    }

    @Requires("contig != null")
    public synchronized boolean hasContig(final String contig) {
        return lastContig == contig || dict.getSequence(contig) != null;
    }

    @Requires("index >= 0")
    public synchronized boolean hasContig(final int index) {
        return lastIndex == index|| dict.getSequence(index) != null;
    }

    @Requires("contig != null")
    @Ensures("result != null")
    public synchronized final SAMSequenceRecord getSequence(final String contig) {
        if ( isCached(contig) )
            return lastSSR;
        else
            return updateCache(contig, -1);
    }

    @Requires("index >= 0")
    @Ensures("result != null")
    public synchronized final SAMSequenceRecord getSequence(final int index) {
        if ( isCached(index) )
            return lastSSR;
        else
            return updateCache(null, index);

    }

    @Requires("contig != null")
    @Ensures("result >= 0")
    public synchronized final int getSequenceIndex(final String contig) {
        if ( ! isCached(contig) ) {
            updateCache(contig, -1);
        }

        return lastIndex;
    }

    @Requires({"contig != null", "lastContig != null"})
    private synchronized boolean isCached(final String contig) {
        return lastContig.equals(contig);
    }

    @Requires({"lastIndex != -1", "index >= 0"})
    private synchronized boolean isCached(final int index) {
        return lastIndex == index;
    }

    /**
     * The key algorithm.  Given a new record, update the last used record, contig
     * name, and index.
     *
     * @param contig
     * @param index
     * @return
     */
    @Requires("contig != null || index >= 0")
    @Ensures("result != null")
    private synchronized SAMSequenceRecord updateCache(final String contig, int index ) {
        SAMSequenceRecord rec = contig == null ? dict.getSequence(index) : dict.getSequence(contig);
        if ( rec == null ) {
            throw new ReviewedStingException("BUG: requested unknown contig=" + contig + " index=" + index);
        } else {
            lastSSR = rec;
            lastContig = rec.getSequenceName();
            lastIndex = rec.getSequenceIndex();
            return rec;
        }
    }


}

Original issue: http://code.google.com/p/cofoja/issues/detail?id=22

[nhatminhle]

From [email protected] on May 20, 2011 09:09:30

Hi, my understanding is this is due to some methods not being synchronized while others are; invariants are invoked for each method and will normally inherit the synchronized property of the method; so it's probably the case that a non-synchronized call checks an invariant while another thread is updating the data structure. Since the first call is not under the monitor lock, that kind of things can happen. Could you try making all your methods synchronized, to see if that's the cause?

We hadn't really thought about this before I guess; so we need to devise a solution but it may take some time to get everybody on the team to agree on a design question. A simple solution would be to provide a @SynchronizedInvariant annotation; another one, maybe better, would be to make invariants synchronized whenever there is a synchronized method in the class, but there's the question of how we handle invariants on classes that inherit synchronized methods, then, which is not exactly clear, so maybe something explicit would be better. David, Leo, Andreas, opinions?

Status: Accepted
Cc: [email protected] [email protected] [email protected]

[nhatminhle]

From [email protected] on May 20, 2011 09:57:04

Do you have multiple MasterSequenceDictionary objects accessing the same SAMSequenceDictionary?

Synchronization of the MasterSequenceDictionary methods only prevents concurrent execution of methods on the same MasterSequenceDictionary instance, it does nothing to prevent two MasterSequenceDictionary instances concurrently accessing the same SAMSequenceDictionary, or to prevent one MasterSequenceDictionary accessing a SAMSequenceDictionary while another class entirely updates it.

If that's the problem then a possible solution would be to make the SAMSequenceDictionary methods synchronized. However, that may not be correct, since you may need to lock on a dict instance over multiple calls to its methods, to ensure it's not updated in between. For contacts we may want to supporting getting arbitrary locks before the precondition is evaluated and releasing them after the postcondition is evaluated.

[nhatminhle]

From [email protected] on May 20, 2011 10:11:00

@david, I don't think that's the problem. Assuming that their synchronization is correct from the start, the problem, on our side, is that invariants are checked on both synchronized AND unsynchronized methods, so even if there's a single MasterSequenceDictionary accessing the object, it can still fail if two different threads call a synchronized and an unsynchronized method on the MasterSequenceDictionary.

The issue is that contracts inherit the attributes of the method they are applied to, and that goes for invariants as well; so if you specify an invariant that would require synchronization and call it from a method that is not synchronized, then the invariant won't be synchronized, which is probably why it's failing.

[nhatminhle]

From [email protected] on May 22, 2011 07:26:51

Yes, I believe (3) is right. One of the methods (getNSequences ) isn't synchronized because the value can never change (the dict is final). But some of the invariants, such as:

dict.getSequence(lastContig).getSequenceIndex() == lastIndex

must be protected by synchronization, as they refer to variables being updated and accessed by multiple threads simultaneously. It would be good to have a contract-level solution to this issue, as simply adding a non-synchronized assessor method to a fully working, thread-safe class could cause the contracts to suddenly fail.

[nhatminhle]

From [email protected] on May 22, 2011 07:51:36

Yes, we should figure something out.

One thing that comes to mind is that if you replaced getNSequences with a public final int field, the type system would know that the value can never change, and invariants obviously wouldn't be checked when it's accessed.

That doesn't fit normal Java style, but it does seem to fit what's needed here.

The bigger issue of multi threading and contracts is not going to have an easy solution, I think. What if you forgot to add synchronized to a method and the code was incorrect because of it? Then, it would make sense for the contracts to fail.

[nhatminhle]

From [email protected] on May 22, 2011 09:04:01

I see two straightforward solutions:

• Either we leave things as they are and people either don't use synchronized invariants or add synchronized to all their methods.
• Or we add something like an @SynchronizedInvariant annotation; we could also warn in case the user uses a simple invariant and has some synchronized methods in her class, but that may be normal.

[nhatminhle]

From [email protected] on May 23, 2011 02:28:06

I don't have a strong opinion on the subject, but I think something explicit as @SynchronizedInvariant may be the best option, since it makes clear to the user what's going on.
Leaving things as they are doesn't sound nice, and I think that automatically making invariants synchronized under some conditions may be confusing.

[nhatminhle]

From [email protected] on May 23, 2011 03:54:12

I chatted to Andreas; let me try to summarize his thoughts on the topic.

• Multithreading makes it much harder to guarantee anything
• As such it does not coexist well with contracts

So you can either

• Weaken the contracts so they're still correct
• or, minimize the part of the code that needs to deal with multi threading, and don't bother writing contracts for that part

This class is kind of a special case, in that by marking everything synchronized you're creating code that doesn't have to worry about multithreading. But the unsynchronized method remains multithreaded and hence unsafe -- it actually doesn't satisfy the invariant.

So the options would be, 1) weaken the invariant, 2) bring the getter into the single threaded zone by marking it multi threaded, 3) bring it into the single threaded zone by making it a field.

I think an invariant with more synchronization than the actual implementation is probably a dangerous thing to introduce.

[nhatminhle]

From [email protected] on May 23, 2011 04:26:22

@david, while I agree on principle, I think, from a practical point of view, none of the proposed solutions is very satisfying from the user's perspective.

I think some sort of built-in support for synchronized may still be desirable, as it would mirror the support that exists for synchronized methods; as I told you earlier when we spoke about it, I think invariants kind of naturally fit into the same scope as methods, so people would expect to be able to synchronize invariants the same way they do for methods.

But yeah, I see your point that making stuff more synchronized than the actual class that'd run without contracts is dangerous because it could hide bugs. I'd like to hear the opinion of the OP on this, actually.

[nhatminhle]

From [email protected] on May 23, 2011 04:27:11

Hi guys,

Just to add a bit on David's summary: I don't know of any simple way to
describe semantics of multi threaded code that is suitable for run time
checking. All attempts I know are horribly complicated (and most not
suitable for runtime checking). IMO this is just another symptom that shows
just how much multi threading f**** up the semantics of programs ): There is
a chance that Hoare logic is a bad concept and there is a chance that multi
threading is a bad concept. I bet the farm on the second (;

Andreas

[nhatminhle]

From [email protected] on May 23, 2011 04:32:34

Just to make it clear that I do agree with David and Andreas (I'm just less of a purist :). The simple model of DbC we use, based on Hoare triplets, is not suitable for multithreading in general; you may be able to describe some very simple conditions (like parameter checking), but no (useful) states at all, so it loses in effectiveness pretty drastically.

[nhatminhle]

From [email protected] on May 23, 2011 04:36:23

I am pretty convinced that any solution we'd be able to come up with will
be a combination of a) slow, b) complex, c) incomplete. I'd be happy to be
proven wrong, but my intuition is that it is probably better remain with a
simple system that works in 90% of the cases rather than having a complex
system that works in 95%. And I am probably rather on the purists side.

While being a purist, I understand that pragmatists change the world (; So
if you come up with a good solution, go for it. I'd just recommend that
you'd double check that it doesn't introduce to many subtle issues.

Andreas