Open lamvak opened 7 years ago
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 notifications@github.com 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 https://github.com/google/thread-weaver/issues/7, or mute the thread https://github.com/notifications/unsubscribe-auth/AIn60Hwx4rL9Oqmfnw-a8HvG4Jibhg_eks5qyXlAgaJpZM4KSJdW .
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