search

aronisstav / Concuerror

OFFICIAL REPOSITORY MOVED:
https://github.com/parapluu/Concuerror
BSD 2-Clause "Simplified" License
1 stars 0 forks source link

Experiment with TransDPOR #29

Closed aronisstav closed 6 years ago

aronisstav commented 6 years ago

Migrating parapluu/Concuerror#172.

According to TransDPOR, if a scheduling is planned in order to reverse a race with a delivery event, a DPOR algorithm can ignore other races for the same delivery event. The intuition is that due to transitivity, "these races" will also appear in future interleavings.

Source DPOR will likely not benefit, as "irrelevant" events will still be initials. Optimal DPOR however, will otherwise add more branches in the wakeup tree.

Idea for experiment: 'freeze' delivery events (i.e. do not add more than one wakeup sequence for them). See if we still find all interleavings.

aronisstav commented 6 years ago

Discussed this a bit with @margnus1 who pointed out that dependencies for optimal DPOR with observers are not transitive in general, so this is an immediate show-stopper there.

aronisstav commented 6 years ago

Forgot to mention that this could still be relevant for other flavors of DPOR but closing this for now.