mine-W privatization undermines Miné, lock is less precise than mine/protection

[sim642]

Our mine-W privatization replaces the mechanism mine uses to convert weak interferences into synchronized ones. However, this W set undermines the precision by not considering locksets at the time of write.

What I'm more surprised about is that lock privatization is less precise than mine and protection on the same example.

TODO

• Try to fix mine-W precision by partitioning by lockset. Simplified to partitioning by mutex which makes lookup at unlock straightforward.
• Figure out why lock is imprecise. Shouldn't it check $$V$$ (or a may variant of it) on unlock or something? Added the same partitioned $$W$$ to lock as well.

[michael-schwarz]

Actually, mine-W is both less and more precise than what Miné has described in his works:

• There is the case you explained above
• But also W is tracked flow-sensitively for us, while it is not in his presentation when using the weak interferences to decide whether to emit a synchronized interference

main:
   lock(a)
   g = ?;
   create(t1);
   g = 5;
   unlock(a);

   lock(a);
   x = g; // Would read top with exclusion based on weak interferences but 5 with W
   unlock(a);

t1:
     // g is T due to other threads...
    lock(a);
    unlock(a); // Creates a synchronized interference (as there is a weak one for g where a is held)

    lock(a);
    g = 5;
    unlock(a);

Now, this of course depends on whether the interferences are accumulated or whether each thread starts out with a blank set of its own interferences at the beginning of each iteration, but it seems like that is not the case.

[sim642]

Indeed, $$W$$ is flow-sensitive while his interference-collecting is not. But doing the partitioning should fix the unintended undermining and just make mine-W slightly more precise in some cases, which I think would be better than the current situation.
We still have mine which actually replicates the interference-collecting (assuming thread IDs), which should boil down to computing $$W$$ as a flow-insensitive unknown.

[...] each thread starts out with a blank set of its own interferences at the beginning of each iteration, but it seems like that is not the case.

He has one set of interferences, but they all have fixed unique thread IDs which the filtering is done by, so effectively each thread has its own empty set to begin with.

The Lock-Centered imprecision is the more debatable matter here though.