New syntax for ghost variables and operations?

MattWindsor91 commented 7 years ago

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 commented 7 years ago

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

septract commented 7 years ago

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 notifications@github.com 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 https://github.com/septract/starling-tool/issues/140#issuecomment-281141198, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9m9gm-FW8UJeVCtC8LyKRWPCZhsRks5redBSgaJpZM4L4UvP .

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

septract / starling-tool

New syntax for ghost variables and operations? #140