Branches in atomic sections, and simplified atomic syntax #142

MattWindsor91 · 2017-02-16T13:24:30Z

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

Simplify atomic syntax
Allow branches in atomic sections (issue Conditionals in atomic sections #141)
Rewrite microcode transformation pipeline (touches on issue Aliasing problem with indices #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 Aliasing problem with indices #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.

Instead of having two atomic syntaxes: ``` <x = y++>; // single atomic action <{ x = y; y = y + 1; }>; // multiple atomic actions ``` We now have a single syntax: ``` <| x = y++; |> // single atomic action <| x = y; y = y + 1; |> // multiple atomic actions ``` Note that the new syntax behaves exactly like a block: it requires semicolons to terminate inner actions, but has no semicolon at the end. This is in preparation for making atomic syntax richer.

This still needs two more changes: 1) Making microcode conditionals sequentially composed instead of parallel composed; 2) Exposing the syntax.

It probably fails 99.9% of tests at the moment. Will pick up after 日本語の勉強.

septract · 2017-02-16T16:21:08Z

Re encoding CAS, can we write this?

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

septract · 2017-02-16T16:24:21Z

...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 · 2017-02-16T17:06:14Z

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 ***@***.***> 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 · 2017-02-17T15:01:58Z

@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 · 2017-02-17T15:11:58Z

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

…

On 17 February 2017 at 15:01, Matt Windsor ***@***.***> 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 <#142 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9mc8xD9Y98fPy5642S2dXxbNBlv8ks5rdbZmgaJpZM4MDAS7> .

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

septract · 2017-02-20T14:45:19Z

Could we look through the code together at some point?

MattWindsor91 · 2017-02-20T16:00:06Z

On 20 Feb 2017, at 14:45, Mike Dodds ***@***.***> 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 · 2017-02-20T17:42:19Z

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

MattWindsor91 · 2017-03-07T11:35:38Z

AST.fs

+        | ACond of
+            cond : Expression
+            * trueBranch : Atomic list
+            * falseBranch : (Atomic list) option


Just adding if (c) { … } else { … } and if (c) { … } to the AST.

MattWindsor91 · 2017-03-07T11:36:11Z

AST.fs

+    /// <summary>
+    ///     Hidden building-blocks for AST pretty-printers.
+    /// </summary>
+    module private Helpers =


This is a F# feature I didn't realise existed until recently. It feels like we should have made more use of this throughout the code!

MattWindsor91 · 2017-03-07T11:36:32Z

AST.fs

+            <+> (maybe
+                    Nop
+                    (fun e -> syntaxStr "else" <+> printBlock pLeg e)
+                    elseLeg)


Abstracted this out because it accounts both for atomic and non-atomic conditionals.

MattWindsor91 · 2017-03-07T11:36:43Z

AST.fs

@@ -290,7 +331,7 @@ module Pretty =
    /// <param name="s">The symbolic to print.</param>
    /// <returns>
    ///     The <see cref="Doc"/> resulting from printing <paramref name="s"/>.
-    /// </returns> 
+    /// </returns>


Space error

MattWindsor91 · 2017-03-07T11:37:21Z

AST.fs

-        braced (ivsep (List.map (pCmd >> Indent) c))
+        | ACond (cond = c; trueBranch = t; falseBranch = f) ->
+            Helpers.printITE printExpression printAtomic c t f
+    and printAtomic (x : Atomic) : Doc = printAtomic' x.Node


Just adding conditionals to the printer. This now needs to be recursive, because conditionals can contain atomics.

MattWindsor91 · 2017-03-07T11:37:34Z

AST.fs

-                                  printBlock printCommand f ])
-                        fo) ]
+        | Command'.If(c, t, f) ->
+            Helpers.printITE printExpression printCommand c t f


Using the new abstraction.

MattWindsor91 · 2017-03-09T16:28:25Z

Grasshopper.fs

@@ -84,7 +89,7 @@ module Types =
        | /// <summary>
          ///     The given microcode command cannot be expressed in Grasshopper.
          /// </summary>
-          CommandNotImplemented of cmd : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list
+          CommandNotImplemented of cmd : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>>


As above, things that used to be ||-composed lists of microcode are now just flattened into single microcode instructions

MattWindsor91 · 2017-03-09T16:29:01Z

Grasshopper.fs

+            String "if"
+            <+> parened (printBoolExprG (printSymGrass printGrassVar) c)
+            <+> printBlock t
+            <+> (if f.IsEmpty then Nop else (String "else" <+> printBlock f))


As well as adding Branch, rearrange this because not every command now needs withSemi.

MattWindsor91 · 2017-03-09T16:29:20Z

Grasshopper.fs

-                id)
+            (traverseMicrocode
+                collectVars
+                (tliftOverExpr collectSymVars))


Going from list list to list.

MattWindsor91 · 2017-03-09T16:31:17Z

Grasshopper.fs

+                    [ printMicrocode
+                         (printCTyped printMarkedVar)
+                         (printSym printMarkedVar)
+                         cmd ]


Removing one level of list

MattWindsor91 · 2017-03-09T16:32:07Z

Grasshopper.fs

@@ -407,75 +417,75 @@ let findTermVars (term : Backends.Z3.Types.ZTerm)
 /// <returns>
 ///     A Chessie result, containing a list of Grasshopper commands.
 /// </returns>
-let grassMicrocode (routine : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list list)
+let rec grassMicrocode (routine : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list)


Going from list list to list, and adding branches introduces recursion.

MattWindsor91 · 2017-03-09T16:33:12Z

Grasshopper.fs

-                fail
-                    (CommandNotImplemented
-                        (cmd = ent,
-                         why = "Cannot encode commands with inner conditionals."))


We now can encode inner conditionals, see line 434 of the new version.

MattWindsor91 · 2017-03-09T16:33:30Z

Grasshopper.fs

+            lift3 (fun c' t' f' -> [ Branch (c', t', f') ])
+                (grassBool c)
+                (grassMicrocode t)
+                (grassMicrocode f)


Branches are new, but distribute.

MattWindsor91 · 2017-03-09T16:33:54Z

Grasshopper.fs

+            ok []
+        (* We can only translate pure assignments and fully spatial
+           (symbolic) assignments. *)
+        | Microcode.Assign (x, Some (Int (_, IVar (Sym s))))


This stuff, I think, has mainly just moved and re-indented.

MattWindsor91 · 2017-03-09T16:35:31Z

Modeller.fs

@@ -805,8 +810,29 @@ and modelBoolExpr
                    | Eq -> mkEq
                    | Neq -> mkNeq
                    | _ -> failwith "unreachable[modelBoolExpr::AnyIn]"
+                (* If at least one of the operands is a symbol, we need to


This new code just tries to make sure that, if one side of an equality/nonequality is a symbol, we try work out its type by modelling the other side first.

This is unrelated to atomic conditionals, I think it's wormed its way into here due to some hacking I was doing around CAV.

MattWindsor91 · 2017-03-09T16:35:52Z

Modeller.fs

        | SymAtomic sym ->
            // TODO(CaptainHayashi): split out.
            let symMR =
                (tryMapSym
                    (wrapMessages BadExpr (modelExpr ctx.Env Full id))
                         sym)
            lift SymC symMR
+        | ACond (cond = c; trueBranch = t; falseBranch = f) ->


New code to allow modelling of atomic conditionals.

MattWindsor91 · 2017-03-09T16:36:17Z

Optimiser.fs

@@ -585,6 +585,10 @@ module Graph =
            | // TODO(CaptainHayashi): is this correct?
              Intrinsic (Havoc v) -> typedVarIsThreadLocal v
            | Stored { Args = ps } -> Seq.forall isLocalArg ps
+            | PrimBranch (trueBranch = t; falseBranch = f) ->


Locality, I think, just distributes through branches.

MattWindsor91 · 2017-03-09T16:36:44Z

Parser.fs

+/// <summary>
+///     Parser for items in a pair of matching brackets.
+///     Automatically parses any whitespace after `bra`, and before `ket`.
+/// </summary>


Lots of boring changes to top-level comments here, but there are important parser changes coming.

MattWindsor91 · 2017-03-09T16:36:56Z

Parser.fs

+/// <summary>
+///     Parser for items in <c><|atomic braces|></c>.
+/// </summary>
+let inAtomicBraces p = inBrackets "<|" "|>" p


The brackets have changed!

MattWindsor91 · 2017-03-09T16:37:18Z

Parser.fs

@@ -90,6 +103,10 @@ let parseView, parseViewRef =
 let parseViewSignature, parseViewSignatureRef =
    createParserForwardedToRef<ViewSignature, unit> ()

+/// Parser for atomic sets.
+let parseAtomic, parseAtomicRef =
+    createParserForwardedToRef<Atomic, unit> ()


Needed because atomics now parse recursively.

MattWindsor91 · 2017-03-09T16:38:02Z

Parser.fs

-        .>>? notFollowedBy (anyOf ";+-")
+        (* A binary operator cannot ever be followed by + or -.
+           This check removes ambiguity between + and ++, and - and --. *)
+        .>>? notFollowedBy (anyOf "+-")


Changing from < > to <| |> means we lose the parser ambiguity formerly induced by < foo = x > 3 >;, so we can simplify this.

MattWindsor91 · 2017-03-09T16:40:49Z

Parser.fs

+            (inBraces pLeg)
+            (opt (pstring "else" >>. ws >>. inBraces pLeg))
+            ctor
+


Abstract out the parser logic for both atomic and non-atomic conditionals.

MattWindsor91 · 2017-03-09T16:41:16Z

Parser.fs

-        <|>
-        // ...or an atomic{} block.
-        (inBraces (many (parseAtomic .>> wsSemi .>> ws))))
+    inAtomicBraces (many1 (parseAtomic .>> ws))


The new syntax knocks both of the old cases into one.

MattWindsor91 · 2017-03-09T16:41:40Z

Parser.fs

-             parseAssume
-             parseCAS
-             parseFetchOrPostfix ]
+             parseIfLike (many1 (parseAtomic .>> ws)) (curry3 ACond)


Atomic conditionals are now a possibility here.

MattWindsor91 · 2017-03-09T16:48:14Z

Parser.fs

 (*
 * Views.
 *)

 /// Parses a conditional view.
 let parseIfView =
+    // TODO: use parseIflike.


This TODO is optional, really. Changing to this would make view conditionals look like

{| if (x) { y } else { z} |}

which is ugly but consistent.

MattWindsor91 · 2017-03-09T16:48:38Z

Parser.fs

@@ -540,7 +558,7 @@ let parsePrimSet =
       2 is easier to spot, so we try it first. *)
    let parseAtomicFirstPrimSet =
        pipe2
-          (parseAtomicSet .>> wsSemi .>> ws)
+          (parseAtomicSet .>> ws)


We no longer require a ; after an atomic block.

MattWindsor91 · 2017-03-09T16:49:29Z

Traversal.fs

@@ -776,6 +776,17 @@ let pushVar (ctx : TraversalContext<'Var>) (v : CTyped<'Var>)
    | c -> fail (ContextMismatch ("vars context", stripVars c))

 /// <summary>
+///     As <see cref="pushVar"/>, but does not crash on invalid context.


This was borne out of frustration mainly, and just means I can get away with not doing a lot of traversal mangling to add and remove contexts just so pushVar works.

MattWindsor91 · 2017-03-09T16:50:27Z

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

MattWindsor91 · 2017-03-09T16:50:45Z

Also, the failing Travis build is due to travis-ci/travis-ci#7401

MattWindsor91 · 2017-03-10T11:28:49Z

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

septract · 2017-03-13T15:57:39Z

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

MattWindsor91 added 15 commits February 13, 2017 12:19

Remove now-redundant backtrack.

0ff6959

Lay groundwork for atomic conditionals.

3bd499a

This still needs two more changes: 1) Making microcode conditionals sequentially composed instead of parallel composed; 2) Exposing the syntax.

Get new microcode processor compiling.

2bf6909

It probably fails 99.9% of tests at the moment. Will pick up after 日本語の勉強.

Fix invalid context bug.

f5f3726

clean up (but not fix) broken after assigner

e7c0ac6

Remove broken writemap stuff.

3f6590a

Try, and fail, to fix broken tests

80500cf

Try and fail to fix _another_ test

08ca5d6

Fix breakages in semantics.

d196c69

Add test for branch equalising.

f586091

Add syntax for atomic branches.

1ffc35d

Make modeller more flexible with ambiguous symbols.

0c923ad

Add some more atomic-branch examples.

8be8082

Revert accidentally changed GH spinlock.

2222a02

MattWindsor91 mentioned this pull request Feb 20, 2017

Relax restrictions on rvalues in atomic sections #147

Open

MattWindsor91 commented Mar 7, 2017

View reviewed changes

MattWindsor91 commented Mar 9, 2017

View reviewed changes

Grasshopper.fs

id)

(traverseMicrocode

collectVars

(tliftOverExpr collectSymVars))

Copy link

Collaborator Author

MattWindsor91 Mar 9, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Going from list list to list.

Remove invalid comment.

25984d3

MattWindsor91 commented Mar 9, 2017

View reviewed changes

Minor comment typo.

40eda22

MattWindsor91 commented Mar 9, 2017

View reviewed changes

MattWindsor91 mentioned this pull request Mar 9, 2017

Massively simplify and equalise primitive commands #150

Open

septract merged commit 8d854aa into master Mar 13, 2017

septract deleted the mw-atomic-conditionals branch March 13, 2017 15:58

Branches in atomic sections, and simplified atomic syntax #142

Branches in atomic sections, and simplified atomic syntax #142

Conversation

MattWindsor91 commented Feb 16, 2017

Simplify atomic syntax

Allow branches in atomic sections

Rewrite microcode translation pipeline

Future work

septract commented Feb 16, 2017

septract commented Feb 16, 2017

MattWindsor91 commented Feb 16, 2017 via email

MattWindsor91 commented Feb 17, 2017

septract commented Feb 17, 2017 via email

septract commented Feb 20, 2017

MattWindsor91 commented Feb 20, 2017 via email

MattWindsor91 commented Feb 20, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MattWindsor91 commented Mar 9, 2017

MattWindsor91 commented Mar 9, 2017

MattWindsor91 commented Mar 10, 2017

septract commented Mar 13, 2017