search

wkschwartz / pigosat

Go (golang) bindings for Picosat, the satisfiability solver
Other
15 stars 4 forks source link

Add Write clausal core / traces and support io.Writer interface #13

Closed justinfx closed 8 years ago

justinfx commented 9 years ago

In this pull request I have added:

All 3 of these methods accept io.Writer, and will internally feed that to the FILE pointer required by the picosat C API

Additionally, Print() has been updated to also accept io.Writer.

wkschwartz commented 9 years ago

I'm intrigued by the idea of using an io.Writer instead of an os.File. We just need to be careful to ensure that the pipes are always getting closed. (I'm sure you did that -- this comment will serve as a note to myself to look for that when I'm reviewing your code, whenever I get to it.)

As always, awesome work. Look forward to reading and testing. Thanks again!

justinfx commented 9 years ago

Good catches on both points. Sorry about that.

I overlooked the race condition, only thinking about acquiring the locks for the UNSAT check. I've fixed that to acquire the lock once for the entire time.

You were also correct that I missed one case of closing the pipe. The read side was always closed, but because the write side of the pipe was being closed at a specific moment to signal the goroutine reader to finish, I overlooked that there was a case where the write pipe would not be closed if the cfdopen() call failed and bailed early. I've added a defer close to the write pipe to make sure both sides are no closed no matter what, when the function scope finishes.

On Thu, Feb 26, 2015 at 4:36 AM William Schwartz notifications@github.com wrote:

I'm intrigued by the idea of using an io.Writer instead of an os.File. We just need to be careful to ensure that the pipes are always getting closed. (I'm sure you did that -- this comment will serve as a note to myself to look for that when I'm reviewing your code, whenever I get to it.)

As always, awesome work. Look forward to reading and testing. Thanks again!

— Reply to this email directly or view it on GitHub https://github.com/wkschwartz/pigosat/pull/13#issuecomment-75981761.

wkschwartz commented 9 years ago

Working on a pull request to merge into your pull request at https://github.com/wkschwartz/pigosat/tree/write-traces. Will submit as a pull request to your fork soon.

justinfx commented 8 years ago

This is an old topic but what was the status of this merge? I just got back to looking at some old code.

wkschwartz commented 8 years ago

@justinfx It turns out I had gotten part way through some edits to this last summer. I have some commits I'd like to add to this PR. I believe you can hit Edit on the PR and click "Allow edits from maintainers" to allow me to post this commits to this branch. I'll have a few more commits to make, but I'd like you to have an opportunity to discuss the changes before I merge them, as this PR was your idea.

Some more things I want to look at

Again, that to do list is just stuff I want to look at. I don't have a real opinion about them yet until I get a chance to look at it.

justinfx commented 8 years ago

Fixed! And yea they tightened up the rules about passing pointers that contains pointers to cgo. But from what I have experience so far, you immediately get compilation errors when you have that situation. You are still allowed to pass pointers as long as they stay alive for the duration of the call and don't also contain pointers.

wkschwartz commented 8 years ago

Still getting permission denied errors. Will try again in a few hours. In the mean time you can take a look at my "assumptions" branch.

On Sunday, September 25, 2016, Justin Israel notifications@github.com wrote:

Fixed! And yea they tightened up the rules about passing pointers that contains pointers to cgo. But from what I have experience so far, you immediately get compilation errors when you have that situation. You are still allowed to pass pointers as long as they stay alive for the duration of the call and don't also contain pointers.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/wkschwartz/pigosat/pull/13#issuecomment-249446333, or mute the thread https://github.com/notifications/unsubscribe-auth/ABWiFQLcHheR7sro2u7Ax9MPFYZzY0cuks5qtuCkgaJpZM4Dlbuk .

William Schwartz cell: 614-578-8007

justinfx commented 8 years ago

In case we got wires crossed, I also allowed edits on #12

wkschwartz commented 8 years ago

Oh now I see why I was confused. My mistake! Thanks!

On Sunday, September 25, 2016, Justin Israel notifications@github.com wrote:

In case we got wires crossed, I also allowed edits on #12 https://github.com/wkschwartz/pigosat/pull/12

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/wkschwartz/pigosat/pull/13#issuecomment-249447227, or mute the thread https://github.com/notifications/unsubscribe-auth/ABWiFSh3tDVC00bZVv-h5dKejvyGuBYDks5qtuSkgaJpZM4Dlbuk .

William Schwartz cell: 614-578-8007

wkschwartz commented 8 years ago

After some confusion on my part about how to close files in cFileWriterWrapper, I now have everything compiling, and the code looks pretty clean at this point, I think.

Two test failures left (TestPrint works), copied below. I'll come back to this tonight or Wednesday, but maybe you can have a think about it first.

--- FAIL: TestWriteClausalCore (0.00s)
    pigosat_test.go:476: Test 1: Expected Unsatisfiable clausal core to start with 'p cnf'; got {"" '\x00' "\x00\x00\x00\x00" "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" '\x00'}
    pigosat_test.go:476: Test 4: Expected Unsatisfiable clausal core to start with 'p cnf'; got {"" '\x00' "\x00\x00\x00\x00" "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" '\x00'}
    pigosat_test.go:476: Test 6: Expected Unsatisfiable clausal core to start with 'p cnf'; got {"" '\x00' "\x00\x00\x00\x00" "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" '\x00'}
    pigosat_test.go:476: Test 7: Expected Unsatisfiable clausal core to start with 'p cnf'; got {"" '\x00' "\x00\x00\x00\x00" "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" '\x00'}
=== RUN   TestWriteTrace
--- FAIL: TestWriteTrace (0.00s)
    pigosat_test.go:500: Test 1: Unsatisfiable formula to produced no compact trace
    pigosat_test.go:514: Test 1: Unsatisfiable formula to produced no extended trace
    pigosat_test.go:500: Test 4: Unsatisfiable formula to produced no compact trace
    pigosat_test.go:514: Test 4: Unsatisfiable formula to produced no extended trace
    pigosat_test.go:500: Test 6: Unsatisfiable formula to produced no compact trace
    pigosat_test.go:514: Test 6: Unsatisfiable formula to produced no extended trace
    pigosat_test.go:500: Test 7: Unsatisfiable formula to produced no compact trace
    pigosat_test.go:514: Test 7: Unsatisfiable formula to produced no extended trace
justinfx commented 8 years ago

http://man7.org/linux/man-pages/man7/pipe.7.html

The parts about a write blocking if the kernel buffer is full is why I did the read in the goroutine and also probably the reason you are getting those test failures. I had the problem at first too where I wasn't getting the output because the read copy never succeeded. Pipe(7) says you shouldn't rely upon platform specific buffer sizes and should read as soon as possible or the write can block if the buffer fills with no reader.

wkschwartz commented 8 years ago

You're absolutely right. My bad.

I just pushed a commit that adds a test for this blocking behavior. The test fails on the current version of the code. I tried switching back to your original goroutine algorithm, but the test is still failing. I'll take another crack at it later. In the meantime, let me know if you see anything wrong with the test.

justinfx commented 8 years ago

I found the cause of the failures. Three things are needed:

1) The change to cfdopen() where the err != nil is causing "Error calling WriteClausalCore: illegal seek" errors for me in the tests. Research into the problem has shown me that checking the error from fdopen() when a valid FILE pointer was returned is causing the problem. When I changed it to simply check cfile == nil and then return the err, it worked again...

2) At this point I am now blocking on TestCFileWriterWrapper. When I reverted the logic back to reading in a goroutine, this stopped blocking.

3) Now I am back to that garbled output from the traces. When I added back in the C.fflush(cfile) after the succesfull write, I get the proper expected output and the tests pass related to the usage of cFileWriterWrapper

justinfx commented 8 years ago

This was where I discovered the hint about reading the error from a succeeded fdopen(): http://comp.unix.programmer.narkive.com/g4gxgYP4/fdopen-cause-illegal-seek

wkschwartz commented 8 years ago

Hopefully this fixes it. I haven't had your problem number 1 but I'm happy to take your word for it because checking whether cfile == nil fits with the documentation anyway. I take it you're running Linux?

As for 2 and 3, I put back your goroutine code and the fflush call.

All the tests pass for me. Take a look and tell me if I missed anything. I'm going to give everything another once-over and if we're both happy, I'll merge.

justinfx commented 8 years ago

I take it you're running Linux?

Ya, I first tested this on my linux box at work, and saw the error right away. It is possible I might not have seen this if I tried it at home on osx

I see you have added back the reading of the pipe in the goroutine, but placed it after the write call. Wouldn't this defeat the purpose? We would want to start the reader before we call write, otherwise write can block and never return.

    // We have to read from the pipe in a separate goroutine because the write
    // end of the pipe will block if the pipe gets full.
    errChan := make(chan error)
    go func() {
        _, e := io.Copy(w, rp)
        errChan <- e
    }()

    if err = writeFn(cfile); err != nil {
        wp.Close()
        return err
    }

Beyond that, I only have one remaining comment. We might want to use a buffered channel here for the read of the pipe:

    errChan := make(chan error, 1)

Because if we were to error and bail out early before <-errChan at the end of the function, we would leak a goroutine. But if we buffer it to a size of one, we expect to only put one return value in there and it will allow the goroutine to finish no matter what.

justinfx commented 8 years ago

Seems like you covered everything I could possibly think of! Awesome. Happy with this when you are. Thanks for the work!!

wkschwartz commented 8 years ago

Again, you're right. I updated the tests to detect the first issue (the order of the goroutine/write calls). I can imagine a test that would cause the channel blocking/goroutine leaking issue, but I don't know how to test for a leaked goroutine.

justinfx commented 8 years ago

Yay! Thanks for all of that hard work.