Skip to content

Commit 35d2c7f

Browse files
committed
Prevent race condition by locking Pigosat object before checking isReady
I can't think of a good way to test this. Open to suggestions.
1 parent d583020 commit 35d2c7f

File tree

1 file changed

+14
-14
lines changed

1 file changed

+14
-14
lines changed

pigosat.go

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -143,11 +143,11 @@ func (p *Pigosat) isReady() bool {
143143
// sure, it's always safe to call Delete again). Most users will not need this
144144
// method.
145145
func (p *Pigosat) Delete() {
146+
p.lock.Lock()
147+
defer p.lock.Unlock()
146148
if !p.isReady() {
147149
return
148150
}
149-
p.lock.Lock()
150-
defer p.lock.Unlock()
151151
// void picosat_reset (PicoSAT *);
152152
C.picosat_reset(p.p)
153153
p.p = nil
@@ -160,34 +160,34 @@ func (p *Pigosat) Delete() {
160160
// Variables returns the number of variables in the formula: The m in the DIMACS
161161
// header "p cnf <m> n".
162162
func (p *Pigosat) Variables() int {
163+
p.lock.RLock()
164+
defer p.lock.RUnlock()
163165
if !p.isReady() {
164166
return 0
165167
}
166-
p.lock.RLock()
167-
defer p.lock.RUnlock()
168168
// int picosat_variables (PicoSAT *);
169169
return int(C.picosat_variables(p.p))
170170
}
171171

172172
// AddedOriginalClauses returns the number of clauses in the formula: The n in
173173
// the DIMACS header "p cnf m <n>".
174174
func (p *Pigosat) AddedOriginalClauses() int {
175+
p.lock.RLock()
176+
defer p.lock.RUnlock()
175177
if !p.isReady() {
176178
return 0
177179
}
178-
p.lock.RLock()
179-
defer p.lock.RUnlock()
180180
// int picosat_added_original_clauses (PicoSAT *);
181181
return int(C.picosat_added_original_clauses(p.p))
182182
}
183183

184184
// Seconds returns the time spent in the PicoSAT library.
185185
func (p *Pigosat) Seconds() time.Duration {
186+
p.lock.RLock()
187+
defer p.lock.RUnlock()
186188
if !p.isReady() {
187189
return 0
188190
}
189-
p.lock.RLock()
190-
defer p.lock.RUnlock()
191191
// double picosat_seconds (PicoSAT *);
192192
return time.Duration(float64(C.picosat_seconds(p.p)) * float64(time.Second))
193193
}
@@ -201,11 +201,11 @@ func (p *Pigosat) Seconds() time.Duration {
201201
// the clause, and causes AddClauses to skip reading the rest of the slice. Nil
202202
// slices are ignored and skipped.
203203
func (p *Pigosat) AddClauses(clauses [][]int32) {
204+
p.lock.Lock()
205+
defer p.lock.Unlock()
204206
if !p.isReady() {
205207
return
206208
}
207-
p.lock.Lock()
208-
defer p.lock.Unlock()
209209
var had0 bool
210210
for _, clause := range clauses {
211211
if len(clause) == 0 {
@@ -249,11 +249,11 @@ func (p *Pigosat) blocksol(sol []bool) {
249249
// // Do stuff with status, solution
250250
// }
251251
func (p *Pigosat) Solve() (status int, solution []bool) {
252+
p.lock.Lock()
253+
defer p.lock.Unlock()
252254
if !p.isReady() {
253255
return NotReady, nil
254256
}
255-
p.lock.Lock()
256-
defer p.lock.Unlock()
257257
// int picosat_sat (PicoSAT *, int decision_limit);
258258
status = int(C.picosat_sat(p.p, -1))
259259
if status == Unsatisfiable || status == Unknown {
@@ -282,11 +282,11 @@ func (p *Pigosat) Solve() (status int, solution []bool) {
282282
// length. There is no need to call BlockSolution after calling Pigosat.Solve,
283283
// which calls it automatically for every Satisfiable solution.
284284
func (p *Pigosat) BlockSolution(solution []bool) error {
285+
p.lock.Lock()
286+
defer p.lock.Unlock()
285287
if !p.isReady() {
286288
return nil
287289
}
288-
p.lock.Lock()
289-
defer p.lock.Unlock()
290290
if n := int(C.picosat_variables(p.p)); len(solution) != n+1 {
291291
return fmt.Errorf("solution length %d, but have %d variables",
292292
len(solution), n)

0 commit comments

Comments
 (0)