Skip to content

Commit

Permalink
Always acquire lock before using PicoSAT object
Browse files Browse the repository at this point in the history
  • Loading branch information
wkschwartz committed Apr 13, 2015
1 parent 141dccb commit 185788d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions pigosat.go
Original file line number Diff line number Diff line change
Expand Up @@ -294,23 +294,23 @@ func (p *Pigosat) Assume(lit Literal) {
// more effective. The function can only be called as long the current
// assumptions are valid. See Assume() for more details.
func (p *Pigosat) FailedAssumption(lit Literal) bool {
defer p.ready(true)()

This comment has been minimized.

Copy link
@justinfx

justinfx Sep 26, 2016

Contributor

Why was this change necessary? Res() is a public function that acquires its own read lock. Do we need to lock twice? I always thought that it is best to not call functions which in turn acquire the lock that was already acquired in the calling function.

This comment has been minimized.

Copy link
@justinfx

justinfx Sep 26, 2016

Contributor

Extra comment... I think of it like this... If Res is public and acquires its own lock, then it is also free to release the read lock and try to acquire the write lock. Do we deadlock?
My opinion is that either the acquire in the calling function should be moved back below again, or an unexported res() should be created which does not lock, and Res() can lock and call it.

// Will SIGABRT if user calls this without the solver being
// in the Unsatisfiable state
if p.Res() != Unsatisfiable {
return false
}
defer p.ready(true)()
return C.picosat_failed_assumption(p.p, C.int(lit)) != 0
}

// Returns a list of failed assumption in the last call to
// Solve(). It only makes sense if the last call to Solve()
// returned Unsatisfiable.
func (p *Pigosat) FailedAssumptions() []Literal {
defer p.ready(true)()
if p.Res() != Unsatisfiable {
return nil
}
defer p.ready(true)()

litPtr := C.picosat_failed_assumptions(p.p)
return p.litArrayToSlice(litPtr)
Expand Down

0 comments on commit 185788d

Please sign in to comment.