Branches in atomic sections, and simplified atomic syntax

[MattWindsor91]

This pull request contains three large changes to Starling's syntax and semantics:

1. Simplify atomic syntax
2. Allow branches in atomic sections (issue #141)
3. Rewrite microcode transformation pipeline (touches on issue #114)

Simplify atomic syntax

Previously, a Starling atomic could be written as <cmd>; if it was one command, or <{cmd1; cmd2; cmdN;}>; if it contained more than one.

This seemed somewhat wasteful and confusing, and mainly happened because the second was an afterthought. This pull request removes the first form and slightly changes the second form, so that atomic commands are now always in the form

<| cmd1; cmd2; cmdN; |> // note the lack of outer semicolon at the end

All of the Pass, Fail, PassGH, and FailGH examples have been rewritten. (None of the WIP ones have, yet.)

Allow branches in atomic sections

Atomic blocks can now contain the form

<| /* ... */ if (condition) { /* atomic block */ } else { /* atomic block */ } /* ... */ |>

which atomically evaluates the conditional and then the appropriate atomic block.

This allows us to write a pure-Starling CAS inline. For example, the CAS in Examples/Pass/spinLock.cvf could be written as:

      {| if test == false then emp else False() |}
        <| if (lock == test) { lock = true; } test = lock; |>
      {| if test == false then holdLock() else emp |}

We can also almost write a heap CAS. This does the same thing as CAS_to_true in Examples/PassGH/spinLock.cvf, but in a slightly convoluted way (see below caveats):

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

Rewrite microcode translation pipeline

To allow 2) to go through, the bit of Starling that converts Microcode into marked, normalised microcode or Boolean relations needed a significant overhaul. This is because previously it assumed any microcode instructions inside a branch (or, indeed, inside a single stored command!) were disjoint, and thus could share the same Intermediate level.

Summary of the changes:

• All microcode instructions are internally sequentially composed now, which fixes the ambiguity in #114 as a side-effect. Two writes to the same variable will always end up executing in the order in which they are given in the microcode;
• Write map building has been removed, because we no longer have the situation where a single microcode write can update more than one bit of an array at the same time;
• Intermediate variables are now only introduced on a per-variable basis when the variable is assigned, which makes for a more efficient use of variables.

Future work

• At this stage it might be worth relaxing the restrictions on atomic assignments to allow, e.g., assignments of arbitrary expressions to thread-locals in atomic blocks. This is why we can't just write the above CAS as

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

• I'm considering changing the view branch syntax to if (x) { y } else { z } for consistency and language simplicity, but this would make views somewhat less readable.

[septract]

Re encoding CAS, can we write this?

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

[septract]

...but in general, it'd be sensible to be able to write an arbitrary expression to a local var. Is there a technical reason we can't do this?

[MattWindsor91]

Currently the rhs of an assignment to a local variable has to be a shared lvalue, so that doesn't work. This is an arbitrary restriction I put in place to make starling atomics have a clear load/store model, and I'm becoming convinced it needs to go.

Sent from my iPhone

On 16 Feb 2017, at 16:21, Mike Dodds notifications@github.com wrote:

Re encoding CAS, can we write this?

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

― You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[MattWindsor91]

@septract aside from the future work, is there anything else suspect about this? It's a fairly large and boring PRQ I'm afraid.

[septract]

Haven't looked through the code yet. The changes all sound entirely sensible.

On 17 February 2017 at 15:01, Matt Windsor notifications@github.com wrote:

@septract https://github.com/septract aside from the future work, is there anything else suspect about this? It's a fairly large and boring PRQ I'm afraid.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/pull/142#issuecomment-280673047, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9mc8xD9Y98fPy5642S2dXxbNBlv8ks5rdbZmgaJpZM4MDAS7 .

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

[septract]

Could we look through the code together at some point?

[MattWindsor91]

On 20 Feb 2017, at 14:45, Mike Dodds notifications@github.com wrote:

Could we look through the code together at some point?

Sorry for late reply. Sure, this would be good. When would be convenient?

[MattWindsor91]

I'm now tracking the separate problem of overly strict assignment restrictions with #147.

[MattWindsor91]

@septract I've tried annotating this code with top-level explanations, mainly as cues for myself when we get to reviewing this :)

[MattWindsor91]

Also, the failing Travis build is due to https://github.com/travis-ci/travis-ci/issues/7401

[MattWindsor91]

@septract it doesn't look like Travis is going to build this reliably any time soon. I'd recommend pulling and testing locally.

[septract]

This looks okay to me, although I haven't grokked the details.