search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Pointers and heap assignment (concept discussion) #148

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

Since GRASShopper is now an integral part of the Starling story, I feel like it's time to consider first-class support for pointers and heap assignment. This would allow us to:

I'll probably propose some syntax in a bit, but I thought I'd get the discussion open.

MattWindsor91 commented 7 years ago

Quick syntax sketch for heap assignment:

<| *PVALUE = EXPR; |>
<| LVALUE = *PVALUE; |>

where PVALUE is an lvalue of pointer type. (We'd have to add pointer types to Starling, but can probably get away with treating them as a scalar type rather than a compound type for now.)

In this case, * would be part of the assignment operator, which is perhaps surprising. I'm not sure of a better way of marking this up though. One possibility that works for the first type is a new assignment operator <- or :=, but I'm not sure how you'd mark up the second type.

septract commented 7 years ago

Hm, I think this is a good idea given infinite time, but is it a priority? Does it let us do something that we can't do now?

On Thursday, 23 February 2017, Matt Windsor notifications@github.com wrote:

Quick syntax sketch for heap assignment:

<| PVALUE = EXPR; |> <| LVALUE = PVALUE; |>

where PVALUE is an lvalue of pointer type. (We'd have to add pointer types to Starling, but can probably get away with treating them as a scalar type rather than a compound type for now.)

In this case, * would be part of the assignment operator, which is perhaps surprising. I'm not sure of a better way of marking this up though. One possibility that works for the first type is a new assignment operator <- or :=, but I'm not sure how you'd mark up the second type.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/148#issuecomment-282060974, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9nC8AI3OfU78KU5Q_Ln7IvIHm1ZHks5rfcFbgaJpZM4MI97T .

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

MattWindsor91 commented 7 years ago

It's not a priority, though it's something I might be tempted to knock together over a few weekends.

The main advantages I can see are:

On the other hand, doing this through symbols is a good demonstration of how flexible Starling is.

septract commented 7 years ago

All noble goals, but they don't add much to your thesis: I'd suggest skipping it and working on better inference.

On 24 February 2017 at 09:04, Matt Windsor notifications@github.com wrote:

It's not a priority, though it's something I might be tempted to knock together over a few weekends.

The main advantages I can see are:

  • Tidier and easier to read proofs (fits with the idea of Starling being a model for 'developer-friendly' tools);
  • Not having to explain or skirt around symbols when explaining Starling to other people;
  • Having a stronger amount of syntax and semantic checking before handing to GRASShopper (ideally, there should never be any GRASShopper syntax errors);
  • Eventually, allowing more optimisations (symbols are a complete black hole when it comes to optimisations; there might be some things we can do with heap writes, but they'd probably be limited to eg. simplifying atomic actions).

On the other hand, doing this through symbols is a good demonstration of how flexible Starling is.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/148#issuecomment-282240619, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9hr9NjkVwaL5xNNJgJMatRAkZ-k7ks5rfp0agaJpZM4MI97T .

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

MattWindsor91 commented 7 years ago

Adding noncritical as per Mike's assessment.