Anchor Error Messages

Anchor checks some fairly complex, subtle properties. While we have tried to ensure that the error messages convery enough information to diagnose their cause, they do take some time to get used to. We provide some examples of errors below to illustrate what they mean and how to approach fixing them.

Validity Errors

Validity errors occur when a synchronization specificatino permits two access to commute in a way that might change program state.

Here is a declaration with a validity violation. The field value can be updated to any value until it becomes -1. At that point, it becomes readonly. The specification indicates that all reads and writes are initially non-movers until value does become -1. At that point, only reads are allowed and are both-movers.

  volatile int value 
      moves_as this.value != -1 ? N : (isRead() ? B : E);

/*****/
class Example {
  volatile int value 
      moves_as this.value != -1 ? N : (isRead() ? B : E);
}
/*****/
VERIFY_BUGGY

Verifying this code identifies a validity problem, and Anchor shows a pair of steps by different threads that commute according to the specification but that change program behavior when they do. The key is to identify those steps and strengthen the specification to prevent them from commuting.

In thise case, a read of -1 can left-commute past a write to the field. However, this is problematic since the field's value might not be -1 before the write occurs, meaning the read will then see a different value. We can rule out the problematic case by permitting reads of -1 to right-commute but not left-commute:

  volatile int value 
      moves_as this.value != -1 ? N : (isRead() ? R : E);

/*****/
class Example {
  volatile int value 
      moves_as this.value != -1 ? N : (isRead() ? R : E);
}
/*****/
VERIFY

Stability Errors

Stability errors occur when writing to one memory location may change a different thread's permission to access a different location in a way that violates Anchor's reduction reasoning.

Synchroniation specification must be stable in that the permission to read or write a field is either invariant over interleaved writes, or at least changd in a way that does not invalidate Anchor's reduction-based reasoning.

Here is a case where stability doesn't hold.

class Example {
  volatile int m  moves_as N;
  int x           moves_as this.m == tid ? B : E;
}

/*****/
/*****/
VERIFY_BUGGY

The error reports identifies several steps that lead to instability. The solution is to strengthen the requirements on when the offending memory location may be modified by other threads.

In this case, we change the specification so that a thread can only change m if m is currently an invalid tid (Tid.nul) and the new value is the current threads tid. Thus, m never becomes the id of a different thread that may try to access x concurrently.

class Example {
  volatile int m  
    moves_as isRead() 
           ? N 
           : (this.m == Tid.null && newValue == tid ? N : E)
    yields_as this.m == tid ==> newValue == tid;

  int x moves_as this.m == tid ?  B : E;
}

/*****/
/*****/
VERIFY

(In this case, we also need to add a yields_as annotation to indicate tha other threads can't "steal" this.m from us.)

Reduction Error

Reduction errors are most often caused by sequences of steps that do not match our reducible pattern:

class Example {
  int value moves_as holds(this) ? B : E;

  public void f() {
    acquire(this);
    this.value = 1;
    release(this);
    acquire(this);
    this.value = 2;
    release(this);
  }
}

/*****/
/*****/
VERIFY_BUGGY

The fix is to change to:

  1. insert a yield if non-atomic behavior is desired;
  2. change the synchronization specifications so accesses can commute as needed; or
  3. change the synchronization operations in the code to eliminate the interference point.

In this case, either (1) or (3) is the likely best option:

  public void f() {
    acquire(this);
    this.value = 1;
    release(this);
    yield;
    acquire(this);
    this.value = 2;
    release(this);
  }

/*****/
class Example {
  int value moves_as holds(this) ? B : E;

  public void f() {
    acquire(this);
    this.value = 1;
    release(this);
    yield;
    acquire(this);
    this.value = 2;
    release(this);
  }
}

/*****/
VERIFY

or:

  public void f() {
    acquire(this);
    this.value = 1;
    this.value = 2;
    release(this);
  }

/*****/
class Example {
  int value moves_as holds(this) ? B : E;

  public void f() {
    acquire(this);
    this.value = 1;
    this.value = 2;
    release(this);
  }
}

/*****/
VERIFY

Loop Reduction Error

Another type of reduction error occurs because Anchor requires that the phase --- either "pre-commit" (matching right movers) or "post-commit" (matching left movers) --- be invariant at loop heads. Thus the following code fails, since we are matching right movers when we first encounter the loop but are maching left movers on the back edge.

class Example {
  public void f() {
    while (true) {
      acquire(this);
      release(this);
    }
  }
}

/*****/
/*****/
VERIFY_BUGGY

If there is not other underlying issue, fixing this typically requires restructuring the loop and/or adding yield:

class Example {
  public void f() {
    while (true) {
      acquire(this);
      release(this);
      yield;
    }
  }  
}

/*****/
/*****/
VERIFY

Volatile Errors

Any field that may be a left, right, or non-mover may be prone to data races.

class Example {
  int value moves_as N;
}

/*****/
/*****/
VERIFY_BUGGY

As such, it must be declared volatile to ensure sequentially consistent behavior.

class Example {
  int value moves_as N;
}

/*****/
/*****/
VERIFY

Array elements cannot be assigned those commutivities. This is a consequence of our Java not having an easy way to make array elements be volatile.

Specification Error

Method returns before completing actions in spec

This happens when Anchor cannot matching the execution of atomic code blocks to steps of the specification. Here is a simple example:

class Example {
  
  volatile int f moves_as N;
   
  modifies this;
  ensures this.f == 1;
  public void f() {
    this.f = 2;
  }  
}

/*****/
/*****/
VERIFY_BUGGY

It can be fixed by ensuring the update to this.f in the code matches the space.

For multi-step specification, Anchor encodes the specification as an NFA and simulates steps in the automata for each yield-free region. Debugging problems when the simulation fails can be a bit tricky.

We expose the the currents state of the NFA in the heap diagrams with special variables $spec$0, $spec$1, etc. that capture the initial state, the state after the first specification block is matched, and so on. You can use those variables to see which states the simulation may be in, which often provides some insight into why the error occurs. For example, in the following, inspecting the pre-state and post-state for the first shows that Anchor matched the first step of the spec to the first block of code (since $spec$0, the initial state became false and $spec$1 became true). Inspecting the information for the return shows, however, that the second step failed to be matched (since spec$1 became false and $spec$2, the accepting state, failed to become true).

class Example {
  
  volatile int f moves_as N;
   
  {
    modifies this;
    ensures this.f == 1;
  } 
  yield;
  {
    modifies this;
    ensures this.f == 2;
  } 
  public void f() {
    this.f = 1;
    yield;
    this.f = 3;
  }  
}

/*****/
/*****/
VERIFY_BUGGY

Again, the fix is to change either the code or the spec so that they match.

Keep in mind that side-effect free code blocks can be ignored during simulation. It's only the ones with side effects that must match specification steps.

Also keep in mind that you should not return early from methods with multi-step specs. That is a current limitation of our translation.

Requires Error

Requires clauses may refer to heap locations but all accesses must be right-movers to ensure that they capture the state visible to the method as it begins executing. Otherwise, when performing reduction, there could be steps interleaved from other threads between when the requires annotations are established and when the code begins executing. This requirement precludes code like the following:

class Example {
  
  volatile int f moves_as write_guarded_by this;
        // or isRead() ? holds(this) ? B : N
        //             : holds(this) ? N : E
    
  requires this.f == 0;
  public void f() {
  }  
}

/*****/
/*****/
VERIFY_BUGGY

The solution is typically to strenghten the specification or add additional requires annotations. In this case, we could require the lock to be held:

requires holds(this);
requires this.f == 0;
public void f()

/*****/
class Example {
  
  volatile int f moves_as write_guarded_by this;
        // or isRead() ? holds(this) ? B : N
        //             : holds(this) ? N : E
    
  requires holds(this);
  requires this.f == 0;
  public void f() {
  }  
}

/*****/
VERIFY

YieldsAs Errors

The yields_as annotation captures all possible values that could be stored in a memory location during a yield by thread tid.

Any yields as annotation must be valid, reflexive, and transitive:

  • It is valid if it captures all possible updates by other threads.
  • It is reflextive if it permits the location to remain unchanged.
  • It is transitive if, given all the yields_as annotations for a program, two yields in a row do not enable any additional values to be stored in the location.

The default yields_as annotation is that the location remains unchanged if thread tid has right-mover read access to it, meaning the read could occur before or after any steps taken by other threads at the yield.

yields_as clause is not valid / reflexive / transitive

These errors occur when one of the three necessary properties is violated. Here's an example that breaks all three:

class YieldsAsBroken {
  volatile int value 
    moves_as isRead() ? N 
                      : (newValue >= this.value ? N : E)
    yields_as this.value != newValue;
}

/*****/
/*****/
VERIFY_BUGGY

The yields_as doesn't admit the case when newValue == this.value, so it is neither valid (since the synchronization specification permits that) nor reflexive. It is not transitive, because the yields_as permits the value to change to a new value by one yield but then change back to the original value in a second yield immediately following the first. We can fix this by simply change the code to the following:

class YieldsAsOK {
  volatile int value 
    moves_as isRead() ? N 
                      : (newValue >= this.value ? N : E)
    yields_as this.value <= newValue;
  }

/*****/
/*****/
VERIFY

Field is not ABA-free

Anchor verifies that such a field exhibits ABA freedom, namely that that the field is never changed from a value A to B and then back to A again, using the yields_as annotation. For example, in the following code snippet the value field is declared noABA, but it does not include a yields_as annotation strong enough to guarantee that it is indeed ABA-free.

class BadNoABA {
  noABA int value  
    moves_as holds(this) 
             ? isRead() ? B 
                          : newValue == this.value + 1 ? B : E
             : E;
} 

/*****/
/*****/
VERIFY_BUGGY

The following yields_as annotation fixes that, because if value is currently A and another thread updates it to a new and distinct value B, it must be that B > A. No thread could change value back to A without violating the field's yields_as specification since it is not the case that B < A.

class NoABA {
  noABA int value
    moves_as holds(this) 
             ? isRead() ? B 
                        : newValue == this.value + 1 ? B : E
             : E;
}

/*****/
/*****/
VERIFY

Loop Termination Errors

An atomic block that reaches it's commit point must reach its end. This requires that Anchor be able to verify that loops appearing in the post-commit phase do indeed finish. You may see several different errors related to this.

Potentially infinite loop head cannot be in post-commit phase

This error means that Anchor did not find a decreasing annotation ensuring that a post-commit loop terminates, as in the following:

class PostCommitLoop {
  volatile int value moves_as N;
  
  public void f() {
    
    // in pre-commit phase
    
    this.value = 1;  
    // in post-commit phase
    
    for (int i = 0; i < 10; i = i + 1) {
      // ...
    }
  }
}

/*****/
/*****/
VERIFY_BUGGY

Even though termination is obvious to us, Anchor still requires it to be documented:

for (int i = 0; i < 10; i = i + 1) 
  decreases 10 - i;
{
    // ...
}

/*****/
class PostCommitLoop {
  volatile int value moves_as N;
  
  public void f() {
    
    // in pre-commit phase
    
    this.value = 1;  
    // in post-commit phase
    
    for (int i = 0; i < 10; i = i + 1) 
      decreases 10 - i;
    {
      // ...
    }
  }
}

/*****/
VERIFY

Loop may not terminate

This error is caused by a decreasing annotation whose expression may increase rather than decrease, as in the following broken version of the above:

for (int i = 0; i < 10; i = i + 1) 
  decreases i;
{
    // ...
}

/*****/
class PostCommitLoop {
  volatile int value moves_as N;
  
  public void f() {
    
    // in pre-commit phase
    
    this.value = 1;  
    // in post-commit phase
    
    for (int i = 0; i < 10; i = i + 1) 
      decreases i;
    {
      // ...
    }
  }
}

/*****/
VERIFY_BUGGY

Decreasing expression not properly bounded by 0

This error is caused by a decreasing annotation whose expression decreases but may also become negative:

int i;
while (i < 10)
  decreases i;
{
    i = i - 1;
}

/*****/
class UnboundedDecreasingLoop {
  public void f() {
    int i;
    while (i < 10)
    decreases i;
    {
        i = i - 1;
    }
  }
}

/*****/
VERIFY_BUGGY