New syntax for ghost variables and operations?

[MattWindsor91]

It might be nice, especially for Vafeiadis-style linearisability proofs, to be able to distinguish between actual code and ghost code syntactically.

Something like (to use the CLH lock as an example):

shared Node tail;
ghost Node head;

// ...

  {| loose(mynode, true) |}
    <{ mypred = tail;
       tail = mynode;
       ghost(%{[|tail|].pred := [|mypred|]}); }>;
  {| queued(mynode, mypred) |}

Starling would statically check against the use of ghost variables in normal code, or ordinary variables as lvalues in ghost code.

[MattWindsor91]

@septract suggests this wouldn't buy us much, if I recall correctly.

[septract]

I think it's only worth doing if we're going to treat ghost code differently somehow. Otherwise what's the point?

…

On Monday, 20 February 2017, Matt Windsor ***@***.***> wrote: @septract <https://github.com/septract> suggests this wouldn't buy us much, if I recall correctly. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#140 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9m9gm-FW8UJeVCtC8LyKRWPCZhsRks5redBSgaJpZM4L4UvP> .

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