search

bblum / landslide-simics

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

What's the right way to handle lockset tracking for semaphores? #163

Open bblum opened 9 years ago

bblum commented 9 years ago

Some semaphores are used as mutexes, in a protocol where the count can never exceed 1.

Some semaphores are squirrel-handed.

Other semaphores are initialized to greater than one. Obvious case of not-a-mutex.

Others are initialized to 1, or 0, or -1, or w/e, and can be treated as mutexes at first, but as soon as someone who doesn't hold the lock does a post, all bets are off. There's no worry to try to track exclusivity in the one-shot message-passing scenario, since happens before covers that.

Seems like this should be sufficient. But there is also the issue of ordering threads so that the bets-off-post comes later than some earlier analysis. If we don't retroactively redo that analysis to ignore that lock being held, there could be false negatives (data races missed).

bblum commented 9 years ago

bdc0d7587a0274c24818918094d43a790360cc53