The stm-promise package

[ Tags: concurrency, lgpl, library ] [ Propose Tags ]

Simple STM Promises for IO computations and external processes. Experimental release.

Example with running the theorem prover eprover in parallel. Given this file structure:

├── mul-commutative
│   ├── induction_x_0.tptp
│   ├── induction_x_1.tptp
│   ├── induction_x_y_0.tptp
│   ├── induction_x_y_1.tptp
│   ├── induction_x_y_2.tptp
│   ├── induction_x_y_3.tptp
│   ├── induction_y_0.tptp
│   ├── induction_y_1.tptp
│   └── no_induction_0.tptp
└── plus-commutative
    ├── induction_x_0.tptp
    ├── induction_x_1.tptp
    ├── induction_x_y_0.tptp
    ├── induction_x_y_1.tptp
    ├── induction_x_y_2.tptp
    ├── induction_x_y_3.tptp
    ├── induction_y_0.tptp
    ├── induction_y_1.tptp
    └── no_induction_0.tptp

We can capture these different obligations and goals with a Control.Concurrent.STM.Promise.Tree.Tree.

file_tree :: Tree FilePath
file_tree = fmap (++ ".tptp") $ tryAll
   [ fmap ("mul-commutative/" ++) $ requireAny
     [ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"]
     , fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"]
     , fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"]
     , Leaf "no_induction_0"
     ]
   , fmap ("plus-commutative/" ++) $ requireAny
     [ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"]
     , fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"]
     , fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"]
     , Leaf "no_induction_0"
     ]
   ]

A successful invocation either contains Theorem or Unsatisfiable.

success :: ProcessResult -> Bool
success r = excode r == ExitSuccess && any (`isInfixOf` stdout r) ok
  where
    ok = ["Theorem","Unsatisfiable"]

Making a promise for an eprover process:

eproverPromise :: FilePath -> IO (Promise [(FilePath,Bool)])
eproverPromise file = do
    let args = ["-xAuto","-tAuto",'-':"-tptp3-format","-s"]
    promise <- processPromise "eprover" (file : args) ""
    let chres :: ProcessResult -> [(FilePath,Bool)]
        chres r = [ (file,success r) ]
    return $ fmap chres promise

Evaluate this in parallel, with a 1 second timeout for each invocation:

main :: IO ()
main = do
    promise_tree <- mapM eproverPromise file_tree

    let timeout      = 1000 * 1000 -- microseconds
        processes    = 2

    workers (Just timeout) processes (interleave promise_tree)

    m_res <- evalTree (any (not . snd)) promise_tree

    let res = fromMaybe [] m_res

    putStrLn "Results: "

    mapM_ print res

The result of this run is:

Results:
("plus-commutative/induction_x_y_0.tptp",True)
("plus-commutative/induction_x_y_1.tptp",True)
("plus-commutative/induction_x_y_2.tptp",True)
("plus-commutative/induction_x_y_3.tptp",True)

This means that four out of four obligations for commutativity of plus succeeded when doing induction on both x and y.

Properties

Versions 0.0.1, 0.0.1.1, 0.0.2, 0.0.3.0, 0.0.3.1
Dependencies base (==4.*), mtl (>=2.1.2 && <3), process (>=1.0.1.1 && <2), stm (>=2.3 && <3) [details]
License LGPL-3
Author Dan Rosén
Maintainer Dan Rosén <danr@chalmers.se>
Category Concurrency
Home page http://www.github.com/danr/stm-promise
Bug tracker http://www.github.com/danr/stm-promise/issues
Source repository head: git clone git://github.com/danr/stm-promise.git
Uploaded Mon Feb 18 12:26:21 UTC 2013 by DanRosen
Distributions NixOS:0.0.3.1
Downloads 1374 total (10 in the last 30 days)
Rating 0.0 (0 ratings) [clear rating]
  • λ
  • λ
  • λ
Status Docs available [build log]
Successful builds reported [all 1 reports]
Hackage Matrix CI

Modules

[Index]

Flags

NameDescriptionDefaultType
werrorDisabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

For package maintainers and hackage trustees