bblum / landslide-simics

the landslide codebase (old simics version)
11 stars 9 forks source link

id - when DR found, add both DR accesses of same pair together in a state space with 2 PPs. #169

Open bblum opened 9 years ago

bblum commented 9 years ago

say we get a DR pair, 0xfoo and 0xbar, found during exploration of mx_lock state space.

current behavior it will generate these new state spaces:

dr 0xfoo
dr 0xfoo, mx_lock
dr 0xbar
dr 0xbar, mx_lock

desired behaviour:

dr 0xfoo
dr 0xbar
dr 0xfoo, dr 0xbar
dr 0xfoo, dr 0xbar, mx_lock
bblum commented 9 years ago

will require altering message_data_race protocol to accept either 1 or 2 eips at once (see landslide/memory.c)