Relax restrictions on rvalues in atomic sections

[MattWindsor91]

Currently any atomic assignment must be either:

• an assign to a thread lvalue from a shared lvalue or symbol (array indices and symbol parameters may be thread expressions, but nothing else); or
• an assign to a shared lvalue from a thread expression (cannot name shared variables at all).

These are arbitrary restrictions I put in place originally to ensure Starling, back before arrays and symbols, had a RISC-style load–store semantics to its atomic commands. The idea was that anything more complicated would need to be entered in as a custom command, making Starling atomics behave very much like processor atomics.

However, since we've now introduced inline conditionals into atomics in #142, we're taking a more freeform approach to what can be modelled in Starling's atomics. Also, until true custom commands are in place, the current system of hard-coded strongly typed shorthands like CAS and ++ is inflexible and brittle.

There isn't any deep reason why these restrictions are here, and they've already resulted in needing to write some fairly janky code to get around them, so I propose we lift them and instead have atomic commands be assignments to any lvalue from any rvalue over both shared and thread environments.

Local commands will continue to be thread environment only, because the assumption that locals are atomic in the meta-theory is based entirely on the inability to observe one thread's locals from another.

[septract]

Agree with this.

…

On Monday, 20 February 2017, Matt Windsor ***@***.***> wrote: Currently any atomic assignment must be either: - an assign to a thread lvalue from a shared lvalue or symbol (array indices and symbol parameters may be thread expressions, but nothing else); *or* - an assign to a shared lvalue from a thread expression (cannot name shared variables at all). These are arbitrary restrictions I put in place originally to ensure Starling, back before arrays and symbols, had a RISC-style load–store semantics to its atomic commands. The idea was that anything more complicated would need to be entered in as a custom command, making Starling atomics behave very much like processor atomics. However, since we've now introduced inline conditionals into atomics in #142 <#142>, we're taking a more freeform approach to what can be modelled in Starling's atomics. Also, until true custom commands are in place, the current system of hard-coded strongly typed shorthands like CAS and ++ is inflexible and brittle. There isn't any deep reason why these restrictions are here, and they've already resulted in needing to write some fairly janky code to get around them, so I propose we lift them and instead have atomic commands be assignments to any lvalue from any rvalue over both shared and thread environments. Local commands will continue to be thread environment only, because the assumption that locals are atomic in the meta-theory is based entirely on the inability to observe one thread's locals from another. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#147>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9mu7Eg_j_e1YZL3hvvPMJw1YAyq7ks5redABgaJpZM4MGdYT> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

Example (though this is predicated on merging #142): in Examples/PassGH/spinLockAtomicBranch.cvf we have (removing an extraneous assignment to test):

      {| isLock(x) |}
        <| test = %{ [|x|].lock };
           if (%{ [|x|].lock } == false) {
               %{ [|x|].lock := true };
           } |>
        test = !test;
      {| if test == false then isLock(x) else holdLock(x) |}

With this change we could write

      {| isLock(x) |}
        <| test = false;
           if (%{ [|x|].lock } == false) {
               test = true;
               %{ [|x|].lock := true };
           } |>
      {| if test == false then isLock(x) else holdLock(x) |}

which is closer to the actual CAS semantics.