Limiting number of interleavings

[lamvak]

Hi,
The code in current shape implies sequential consistency (due to locking after each byte code instruction). This way the analysis is fully reliable only when there are no data races - as defined in JMM https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5

There is work outlining a different approach to interleavings using only locations where the happens-before relation is forced (i.e. lockin / unlocking the same monitor, acess to a volatile variable, etc.). See https://www.cs.rice.edu/~javaplt/papers/ricken-phd-thesis.pdf

This optimization in number of interleavings, enclosing whole critical blocks, could be considered in Thread Weaver - it seems that with already assumed sequential consistency there would be no loss of reliability.
Please, let me know if the above seem a fair statement. I would happily try to tackle this.
Marcin

[alasdairmackintosh]

Thanks for the message. I'll take a look at the links you sent, and will
try to get back to you in a few days.

Alasdair

On Sun, Oct 9, 2016 at 4:31 PM, lamvak [email protected] wrote:

Hi,
The code in current shape implies sequential consistency (due to locking
after each byte code instruction). This way the analysis is fully reliable
only when there are no data races - as defined in JMM
https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5

There is work outlining a different approach to interleavings using only
locations where the happens-before relation is forced (i.e. lockin /
unlocking the same monitor, acess to a volatile variable, etc.). See
https://www.cs.rice.edu/~javaplt/papers/ricken-phd-thesis.pdf

This optimization in number of interleavings, enclosing whole critical
blocks, could be considered in Thread Weaver - it seems that with already
assumed sequential consistency there would be no loss of reliability.
Please, let me know if the above seem a fair statement. I would happily
try to tackle this.
Marcin

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#7, or mute the thread
https://github.com/notifications/unsubscribe-auth/AIn60Hwx4rL9Oqmfnw-a8HvG4Jibhg_eks5qyXlAgaJpZM4KSJdW
.