fmjs / emme Goto Github PK

Hi Cristian!

I've found EMME very useful for double-checking expectations I've had about the JS memory model. I currently believe that the JS spec mis-specifies "Init" actions, and I tried to use EMME to confirm that the pathological executions I was expecting were exhibited, but it's not giving the output I was expecting.

For the following test, with en_SINGLE_WRITES disabled, I expected to observe 4 valid executions, for each bytewise combination of thread 2 reading from the init event/thread 1's write.
test.zip (see test.bex in the zip)

However, EMME only reported 2 executions, where thread 2 reads from one or the other, but never a bytewise combination. Graphs are included in the above zip.

However, if I add an unrelated read event on a different thread, at a disjoint section of the arraybuffer, I get the 4 executions I was expecting.
test_unrelated_read.zip (see test.bex in the zip)

This seems to be affected by the tear-free reads predicate. In the first example, if I comment this predicate out of the model, I observe the 4 executions I'm expecting. I don't believe that the tear-free reads condition should affect my test, since "Init" events are specified as being one byte in size.