Some expected executions not observed when en_SINGLE_WRITES disabled

[conrad-watt]

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.

[cristian-mattarei]

Hi Conrad,
the fact that adding another unrelated event to the program impacts the set of valid executions is pretty interesting, I will have a look at that.
Regarding the size of init events, in EMME they are set equal to the largest possible memory operation on that shared array buffer, e.g., read(x-16, 1) implies that the size of init(x) is 32-bits. Do you have a reference for the fact that init events are 1 byte in size?

[cristian-mattarei]

Hi Conrad,
the possible executions change when you add the print(x-I16[2]) event because you are also implicitly changing the size of the init event, thus affecting the scope of the tear-free read predicate. In fact, if the unrelated event operates in the bytes 0..1 (e.g., print(x-I16[0]), or print(x-I8[1])) then the set of valid executions do not change.

[conrad-watt]

Hi Cristian

In the current specification, AllocateSharedArrayBuffer inserts Init events covering the length of the buffer through CreateSharedByteDataBlock, with each Init event being a single-byte write of the value 0: https://tc39.github.io/ecma262/#sec-createsharedbytedatablock. This is the only place I can find in the spec where Init events are used.

[cristian-mattarei]

The CreateSharedByteDataBlock( size ) is parameterized on the size of the SharedArrayBuffer. In fact, the function initializes to 0 every byte (see for loop at step 6.).

[conrad-watt]

But each byte is initialised in the loop with a separate 1-byte Init event, not one Init event covering the entire size. If I'm interpreting the spec correctly, this means that a 2-byte read event can read-from an aligned 2-byte write event, but still tear with the init event(s), since it appears in the model as two 1-byte writes.

That being said, I don't think the informal intention of the spec authors was to allow this behaviour (I think it's a bug and am planning to draft a normative PR) - I was just expecting to observe it in EMME to confirm I hadn't misread the spec.

[cristian-mattarei]

Now I see your point. I have added a new branch that supports the multiple init values (https://github.com/FMJS/EMME/tree/multiple_inits).

[conrad-watt]

Thanks for the quick response! I'll have a play around with this.