We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 7e98213 commit 1b4beaeCopy full SHA for 1b4beae
src/analyses/pthreadBarriers.ml
@@ -79,13 +79,6 @@ struct
79
let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
80
if Z.leq min_cap Z.one then
81
true, must
82
- else if min_cap = Z.of_int 2 && count = 1 then
83
- let elem = Waiters.choose relevant_waiters in
84
- let curr = MustObserved.find (MHPplusLock.tid elem) must in
85
- let must' = MustObserved.add (MHPplusLock.tid elem) (Barriers.add addr curr) must in
86
- true, must'
87
- else if min_cap = Z.of_int 2 && count >= 1 then
88
- true, must
89
else if Z.geq (Z.of_int (count + 1)) min_cap then
90
(* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that
91
MHP is pairwise true? This solution is a sledgehammer, there should be something much
0 commit comments