Skip to content

Massively simplify and equalise primitive commands #150

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
MattWindsor91 wants to merge 13 commits into
base: master
Choose a base branch
from
Open

Massively simplify and equalise primitive commands #150

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
809a761
Remove assignment types.
MattWindsor91 Mar 7, 2017
af3f42a
Fix some lints in Modeller.
MattWindsor91 Mar 7, 2017
bfad3a2
Merge PrimCommand and Microcode.
MattWindsor91 Mar 8, 2017
81398c7
Add regression units for local commands.
MattWindsor91 Mar 8, 2017
0188a6b
Add test for normal integer assign atomics.
MattWindsor91 Mar 8, 2017
e61578c
Remove useless ILoad/BLoad stored commands.
MattWindsor91 Mar 8, 2017
4f67cbe
Relax and simplify atomic modelling.
MattWindsor91 Mar 8, 2017
fc57990
Tidy up tests.
MattWindsor91 Mar 9, 2017
c644da4
Move atomic modellers into their own module.
MattWindsor91 Mar 9, 2017
80e0f96
Remove stored increment/decrement commands.
MattWindsor91 Mar 9, 2017
4372a3f
Unify local and atomic primitive command sets.
MattWindsor91 Mar 9, 2017
2a9352a
Remove dead code.
MattWindsor91 Mar 9, 2017
cd686b2
Rewrite GH atomic-branch spinlock to implement CAS properly.
MattWindsor91 Mar 9, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 34 additions & 15 deletions AST.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,10 @@ module Types =
| ArraySubscript of array : Expression * subscript : Expression
and Expression = Node<Expression'>

/// An atomic action.
type Atomic' =
/// <summary>
/// A primitive command.
/// </summary>
type Prim' =
| CompareAndSwap of
src : Expression
* test : Expression
Expand All @@ -71,8 +73,13 @@ module Types =
| Postfix of Expression * FetchMode // <a++> or <a-->
| Id // <id>
| Assume of Expression // <assume(e)>
| SymAtomic of symbol : Symbolic<Expression> // %{xyz}(x, y)
| SymCommand of symbol : Symbolic<Expression> // %{xyz}(x, y)
| Havoc of var : string // havoc var
and Prim = Node<Prim'>

/// An atomic action.
type Atomic' =
| APrim of Prim
| ACond of
cond : Expression
* trueBranch : Atomic list
Expand Down Expand Up @@ -177,9 +184,9 @@ module Types =

/// A set of primitives.
type PrimSet =
{ PreAssigns: (Expression * Expression) list
{ PreLocals: Prim list
Atomics: Atomic list
PostAssigns: (Expression * Expression) list }
PostLocals: Prim list }

/// A statement in the command language.
type Command' =
Expand Down Expand Up @@ -401,14 +408,14 @@ module Pretty =
equality (printExpression dest) (printExpression src)

/// <summary>
/// Pretty-prints atomic actions.
/// Pretty-prints primitive actions.
/// </summary>
/// <param name="a">The <see cref="Atomic'"/> to print.</param>
/// <param name="p">The <see cref="Prim'"/> to print.</param>
/// <returns>
/// A <see cref="Doc"/> representing <paramref name="a"/>.
/// A <see cref="Doc"/> representing <paramref name="p"/>.
/// </returns>
let rec printAtomic' (a : Atomic') : Doc =
match a with
let rec printPrim' (p : Prim') : Doc =
match p with
| CompareAndSwap(l, f, t) ->
func "CAS" [ printExpression l
printExpression f
Expand All @@ -421,8 +428,20 @@ module Pretty =
hjoin [ printExpression l; printFetchMode m ]
| Id -> String "id"
| Assume e -> func "assume" [ printExpression e ]
| SymAtomic sym -> printSymbolic sym
| SymCommand sym -> printSymbolic sym
| Havoc var -> String "havoc" <+> String var
and printPrim (x : Prim) : Doc = printPrim' x.Node

/// <summary>
/// Pretty-prints atomic actions.
/// </summary>
/// <param name="a">The <see cref="Atomic'"/> to print.</param>
/// <returns>
/// A <see cref="Doc"/> representing <paramref name="a"/>.
/// </returns>
let rec printAtomic' (a : Atomic') : Doc =
match a with
| APrim p -> printPrim p
| ACond (cond = c; trueBranch = t; falseBranch = f) ->
Helpers.printITE printExpression printAtomic c t f
and printAtomic (x : Atomic) : Doc = printAtomic' x.Node
Expand All @@ -433,12 +452,12 @@ module Pretty =
(* The trick here is to make Prim [] appear as ;, but
Prim [x; y; z] appear as x; y; z;, and to do the same with
atomic lists. *)
| Command'.Prim { PreAssigns = ps; Atomics = ts; PostAssigns = qs } ->
seq { yield! Seq.map (uncurry printAssign) ps
| Command'.Prim { PreLocals = ps; Atomics = ts; PostLocals = qs } ->
seq { yield! Seq.map printPrim ps
yield (ts
|> Seq.map printAtomic
|> semiSep |> withSemi |> braced |> angled)
yield! Seq.map (uncurry printAssign) qs }
yield! Seq.map printPrim qs }
|> semiSep |> withSemi
| Command'.If(c, t, f) ->
Helpers.printITE printExpression printCommand c t f
Expand Down Expand Up @@ -592,7 +611,7 @@ let (|BoolExp'|ArithExp'|AnyExp'|) (e : Expression')
| ArraySubscript _ -> AnyExp' e
| Num _ -> ArithExp' e
| True | False -> BoolExp' e
| BopExpr(BoolOp, _, _) | UopExpr(_,_) -> BoolExp' e
| BopExpr(BoolOp, _, _) | UopExpr(_) -> BoolExp' e
| BopExpr(ArithOp, _, _) -> ArithExp' e

/// Active pattern classifying expressions as to whether they are
Expand Down
22 changes: 13 additions & 9 deletions Collator.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,8 +188,8 @@ module ParamDesugar =
let rewriteAFunc { Name = n; Params = ps } =
{ Name = n; Params = List.map rewriteExpression ps }

let rec rewriteAtomic atom =
let rewriteAtomic' =
let rec rewritePrim prim =
let rewritePrim' =
function
| CompareAndSwap (src, test, dest) ->
CompareAndSwap (rewriteExpression src, rewriteExpression test, rewriteExpression dest)
Expand All @@ -199,22 +199,26 @@ module ParamDesugar =
Postfix (rewriteExpression e, fm)
| Id -> Id
| Assume e -> Assume (rewriteExpression e)
| SymAtomic sym ->
SymAtomic (rewriteSymbolic sym)
| SymCommand sym ->
SymCommand (rewriteSymbolic sym)
| Havoc v -> Havoc (rewriteVar v)
{ prim with Node = rewritePrim' prim.Node }

let rec rewriteAtomic atom =
let rewriteAtomic' =
function
| APrim p -> APrim (rewritePrim p)
| ACond (cond = c; trueBranch = t; falseBranch = f) ->
ACond
(rewriteExpression c,
List.map rewriteAtomic t,
Option.map (List.map rewriteAtomic) f)
{ atom with Node = rewriteAtomic' atom.Node }

let rewritePrimSet { PreAssigns = ps; Atomics = ts; PostAssigns = qs } =
let rewriteAssign = pairMap rewriteExpression rewriteExpression

{ PreAssigns = List.map rewriteAssign ps
let rewritePrimSet { PreLocals = ps; Atomics = ts; PostLocals = qs } =
{ PreLocals = List.map rewritePrim ps
Atomics = List.map rewriteAtomic ts
PostAssigns = List.map rewriteAssign qs }
PostLocals = List.map rewritePrim qs }

let rec rewriteView =
function
Expand Down
Loading