Semantic of Multiple Assignments

[DavePearce]

An interesting question raised by @utting is what the real semantics for multiple assignments of the form x,y = e1,e2 are. For example, what about these statements:

x,x = x,y
a[i],a[j] = 1,2
*p, *q = 1,2

The question here is: what does it mean when the left-hand sides are not disjoint?

IDEA: One approach here is to require that they are disjoint. This would mean, for example, introducing proof obligations to establish that they are.

NOTES: The general assumption has been that the evaluation order follows left-to-right. Hence, all left-hand sides are evaluated first, then all right-hand sides and, finally, the assignment occurs (atomically).

[DavePearce]

An interesting example is swap:

method swap(&int x, &int y):
   *x, *y = *y, *x

This method would fail the disjointness test but, in reality, it's fine for the case when they are the same. Maybe this doesn't matter because we can always code it using a temporary variable.

[DavePearce]

NOTES: if I persist with making the assignment atomic, then realistically it will need a disjointness requirement. Otherwise, it doesn't make sense to atomically assign two things to the same variable. I suppose one could argue that we can simply introduce a "race condition" whereby we don't know which it is. But, this seems wrong to me!!

[DavePearce]

One reason for making it atomic is to enable the possibility that it compiles down to a single Compare And Swap instruction. For example, this could compile down:

&int x = ..
int y = ...
bool f = ...
//    
*x, f = y, (*x == y)

This is not a valid implementation of compare and swap, however, as there is no conditional assignment. I'm not sure whether or not it's enough.

[DavePearce]

Curiously enough, it seems that the Whiley verifier already handles this following a non-atomic approach where by the assignments are made in left-to-right order. The following illustrates:

method f(int x, int y) -> (int r)
ensures r == y:
    //
    x,x = 1,y
    //
    return x

This verifies. However, swapping the right-hand side to y,1 and it does not.

[DavePearce]

Another interesting example is the following which, correctly, fails to verify:

type uint is (int x) where x >= 0

method f(int[] arr, uint i, uint j) -> (int r)
// indices must be within bounds
requires i < |arr| && j < |arr|
// return value must be zero
ensures 0 == r:
    //
    arr[j],arr[i] = 0,1
    //
    return arr[j]

[DavePearce]

This should be written up as RFC and added the language specification?

[DavePearce]

Migrated to Whiley/RFCs#44