JMM actions to statements transition

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

JMM actions to statements transition

Sergey Zaytsev
Hi all. Can somebody , please, bring some light on JMM actions ? How can one use such abstract term like "action" to argue about correctness or possible results, since there is no strict definition is term "action" ?

I mean is volatile read simply equals to var local = va and volatile write action to va = "some value" ?

Sergey
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: JMM actions to statements transition

Martin Buchholz-3
There is an attempt to define them in the jls (but it's hard to understand)
People don't think about "actions", but do think about "synchronization actions".

On Thu, Jul 7, 2016 at 9:00 AM, Sergey Zaytsev <[hidden email]> wrote:
Hi all. Can somebody , please, bring some light on JMM actions ? How can one use such abstract term like "action" to argue about correctness or possible results, since there is no strict definition is term "action" ?

I mean is volatile read simply equals to var local = va and volatile write action to va = "some value" ?

Sergey
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: JMM actions to statements transition

Aleksey Shipilev-2
In reply to this post by Sergey Zaytsev
On 07/07/2016 07:00 PM, Sergey Zaytsev wrote:
> Hi all. Can somebody , please, bring some light on JMM actions ? How
> can one use such abstract term like "action" to argue about
> correctness or possible results, since there is no strict definition
> is term "action" ?

What do you mean "no strict definition"? There is JLS 17.4.2 "Actions"
that enumerate them.


> I mean is volatile read simply equals to var local = va and volatile
> write action to va = "some value" ?

This is where it gets messy. Actions and program statements are
connected with program order. More precisely, out of the entire "soup of
executions" that you may construct with arbitrary actions, you can only
select those executions where the actions of one particular thread can
be derived from the original program, to reason about that particular
program outcomes.

I thought I explained it here:
  https://shipilev.net/blog/2014/jmm-pragmatics/#_java_memory_model

Thanks,
-Aleksey


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

signature.asc (836 bytes) Download Attachment