search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Use pure `solve` function #110

Closed VictorCMiraldo closed 2 years ago

VictorCMiraldo commented 2 years ago

Using a pure solve function and parallel symbolic evaluation seems promising; our state monad is hurting us a little, I might work on removing that state monad if not extremely necessary.

Also, another curious fact is that keeping the lock in pushMStack and popMStack causes a deadlock, but removing it makes everything go through. I'm a bit puzzled by it.

VictorCMiraldo commented 2 years ago

@0xd34df00d, a quick google gave me this: https://stackoverflow.com/questions/23471594/concurrent-stack-implementation-using-mvar/23499300#23499300

0xd34df00d commented 2 years ago

@0xd34df00d, a quick google gave me this: https://stackoverflow.com/questions/23471594/concurrent-stack-implementation-using-mvar/23499300#23499300

Oh welp, noticed this just now, sorry! Anyway, using QSem seems cleaner than what's in that answer.

serras commented 2 years ago

Did GitHub get confused by the two PRs?

VictorCMiraldo commented 2 years ago

Either GitHub, Git or I got confused by the two PRs; I rebased this branch not inclusing the two initial commits on the latest dev (after merging #109) but now the web interface shows more commits than it should

serras commented 2 years ago

I think it's good now. I know that if you force-push GitHub leaves anything above it unchanged, but the Files tab work as it should.

VictorCMiraldo commented 2 years ago

For the record; it's remarkable that Pirouette is significantly simpler and faster! This is CI's time for the isUnity test:

      isUnity Bug
        [correct_isUnity v] validate [\r _ -> r] counter: OK (2.71s)

A few PRs ago we were close to 10s! :tada: