Comparisons with other static approaches

We compare below the musketeer to the previous static techniques that we reimplemented. We exercise the different implementations on the benchmarks classic, fast and debian for TSO. In the table, (m) is our tool musketeer. (p) is the delay set analysis of Pensieve. (v) is the Visual Studio policy. (e) places a fence after each access to shared memory. (n) is the naive method of [19, p. 288], i.e. a fence on each delay.

A short analysis of these results regarding the precision:

• the Visual Studio (unsound in general) would infer 38 fences for memcached against 18 by musketeer (see (V) and (M)).
• The times between musketeer and pensieve are comparable but musketeer is much more precise (see (P) and (M)).
• The method could have appeared too imprecise to be used on larger programs. We note it is not the case. Indeed,
  • we applied musketeer to large programs (e.g. memcached). As Section 2 of the paper shows, the overhead between memcached fenced by musketeer and without fences is very low. Thus musketeer is precise enough to not insert too many fences; otherwise this overhead would be much higher.
  • as the table shows, musketeer is the most precise of the sound methods.