search

AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

[RFC] Local volatile variables in SPARK #10

Closed yannickmoy closed 5 years ago

yannickmoy commented 5 years ago

In connection with internal AdaCore tickets R604-012 and S504-004 from SPARK customers.

kanigsson commented 5 years ago

Just one comment for now: instead of using "volatile" in this way, could one imagine an aspect or pragma in compiler that indicates "no compiler optimization"? So instead of

Cond : Boolean with Volatile;

we would have

Cond : Boolean with No_Optimization;

This would be a compiler change rather than a SPARK language change.

Edit I now have read the section "Rationale and Alternatives", and probably I don't appreciate the complexity of this approach, but still this seems like the proper solution, while this one here looks like a hack

yannickmoy commented 5 years ago

I agree with Johannes that adding a No_Optimization aspect equivalent to Volatile just for the compiler would work as well.

kanigsson commented 5 years ago

I understand the proposal now. But do we really need to link volatile on local variables to the four SPARK volatility properties?

A simpler proposal could be like this:

sttaft commented 5 years ago

The advantage of using a new pragma/aspect rather than simply making a "local' volatile implicitly being treated as simply "no-optim" is that you will be less likely to hide bugs. If you give this implicit meaning to a local volatile, existing code might use volatile on a local variable and expect the normal Ada semantics, which is not the same as "no-optim." When you SPARK-ify this existing code, the local use of volatile would remain legal, but have different semantics.

-Tuck

On Thu, May 9, 2019 at 7:23 PM Johannes Kanig notifications@github.com wrote:

I understand the proposal now. But do we really need to link volatile on local variables to the four SPARK volatility properties?

A simpler proposal could be like this:

  • it is allowed to put a pragma volatile on local variables
  • the pragma is ignored by the SPARK tool
  • is disallowed for actual external effects/allowed only to disable compiler optimizations
  • it's not needed/allowed to specify the four volatile properties

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/10#issuecomment-491101400, or mute the thread https://github.com/notifications/unsubscribe-auth/AANZ4FNNFJJG64PU5SXJCUDPUSW6PANCNFSM4HLKF45Q .

kanigsson commented 5 years ago

Just to be clear I also would prefer the new pragma/aspect. I'm just saying that I find the current proposal needlessly complex, and I don't see the difference with my simpler proposal.

sttaft commented 5 years ago

My only point was that using Volatile on a local variable to automatically imply "No_Optimize" might be more error prone, since if the code were debugged using Ada before shifting into SPARK mode, the semantics of the local volatile variable would change pretty significantly. We don't usually want the addition or removal of SPARK mode to have such a major effect on semantics.

-Tuck

On Thu, May 9, 2019 at 10:10 PM Johannes Kanig notifications@github.com wrote:

Just to be clear I also would prefer the new pragma/aspect. I'm just saying that I find the current proposal needlessly complex, and I don't see the difference with my simpler proposal.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/10#issuecomment-491128560, or mute the thread https://github.com/notifications/unsubscribe-auth/AANZ4FN2M6HAJEP7AMPXWN3PUTKP7ANCNFSM4HLKF45Q .

clairedross commented 5 years ago

I understand the proposal now. But do we really need to link volatile on local variables to the four SPARK volatility properties?

A simpler proposal could be like this:

  • it is allowed to put a pragma volatile on local variables
  • the pragma is ignored by the SPARK tool
  • is disallowed for actual external effects/allowed only to disable compiler optimizations
  • it's not needed/allowed to specify the four volatile properties

Or we force to specify that all four volatile properties are false.

yannickmoy commented 5 years ago

I have amended the proposal to take objections into account. So the new proposal is to have a new volatility property No_Caching in addition to having all other volatility properties set to False.