Java Atomics

[pieter-bos]

Previously, classes whose name started with "Atomic" were treated in a special way, where its methods are treated as atomic actions. Do we want to support anything like that again?

[bobismijnnaam]

I had an idea to support "inline" methods, i.e. methods that are inlined at their call site and hence don't need contracts. Then the good part about this would be that you can pass code blocks as arguments, mostly to do proof steps. These code blocks should be kind of inline lambda's so you can pass values to them. E.g. (apologies for the hideous syntax):

class AtomicInteger {
  //@ given (int -> code) fail;
  //@ given (int -> code) succ
  public /*@ vercors_inline @*/ bool cas(int expected, int new) {
    synchronized (this) {
      if (val == expected) {
        expected = new;
        //@ inline_call succ(\old(val))
        return true;
      }
      //@ inline_call fail(val);
      return false;
    }
  }
}

...

myAtomicInt.cas(0, 1) /* given { succ = { oldVal => /* change lock invariant or something based on oldVal? */ } } */;

So in a sense, that would be the user-available generalization of what we had before.