Implement an experimental parmap operation.

This is semantically the same as `map` on finite sequences,
but forks a separate Haskell thread for each element of the sequence.
When the GHC runtime is instructed to use multiple OS threads,
data-parallel exeuction can be achieved.

lib/Cryptol.cry

@@ -923,6 +923,17 @@ pmod x y = if y == 0 then 0/0 else last zs
     zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
 
 
+// Experimental primitives ------------------------------------------------------------
+
+/**
+ * Parallel map.  The given function is applied to each element in the
+ * given finite seqeuence, and the results are computed in parallel.
+ *
+ * This function is experimental.
+ */
+primitive parmap : {a, b, n} (fin n) => (a -> b) -> [n]a -> [n]b
+
+
 // Utility operations -----------------------------------------------------------------
 
 /**

src/Cryptol/Eval/Backend.hs

@@ -235,6 +235,11 @@ class MonadIO (SEval sym) => Backend sym where
   --   its own evaluation.
   sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
 
+  -- | Begin evaluating the given computation eagerly in a separate thread
+  --   and return a thunk which will await the completion of the given computation
+  --   when forced.
+  sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)
+
   -- | Merge the two given computations according to the predicate.
   mergeEval ::
      sym ->

src/Cryptol/Eval/Concrete.hs

@@ -301,6 +301,9 @@ primTable = let sym = Concrete in
                     updatePrim sym updateBack_word updateBack)
 
     -- Misc
+  , ("parmap"     , {-# SCC "Prelude::parmap" #-}
+                    parmapV sym)
+
   , ("fromZ"      , {-# SCC "Prelude::fromZ" #-}
                     fromZV sym)
 

src/Cryptol/Eval/Concrete/Value.hs

@@ -161,6 +161,7 @@ instance Backend Concrete where
 
   sDeclareHole _ = blackhole
   sDelayFill _ = delayFill
+  sSpark _ = evalSpark
 
   ppBit _ b | b         = text "True"
             | otherwise = text "False"

src/Cryptol/Eval/Generic.hs

@@ -1908,7 +1908,38 @@ mergeSeqMap sym c x y =
     iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)
 
 
+--------------------------------------------------------------------------------
+-- Experimental parallel primitives
 
+parmapV :: Backend sym => sym -> GenValue sym
+parmapV sym =
+  tlam $ \_a ->
+  tlam $ \_b ->
+  ilam $ \_n ->
+  lam $ \f -> pure $
+  lam $ \xs ->
+    do f' <- fromVFun <$> f
+       xs' <- xs
+       case xs' of
+          VWord n w ->
+            do m <- asBitsMap sym <$> w
+               m' <- sparkParMap sym f' n m
+               pure (VWord n (pure (LargeBitsVal n m')))
+          VSeq n m ->
+            VSeq n <$> sparkParMap sym f' n m
+
+          _ -> panic "parmapV" ["expected sequence!"]
+
+
+sparkParMap ::
+  Backend sym =>
+  sym ->
+  (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) ->
+  Integer ->
+  SeqMap sym ->
+  SEval sym (SeqMap sym)
+sparkParMap sym f n m =
+  finiteSeqMap sym <$> mapM (sSpark sym . f) (enumerateSeqMap n m)
 
 --------------------------------------------------------------------------------
 -- Floating Point Operations
@@ -1932,7 +1963,3 @@ fpRndRNA sym = wordLit sym 3 1 {- to nearest, ties to away from 0 -}
 fpRndRTP sym = wordLit sym 3 2 {- to +inf -}
 fpRndRTN sym = wordLit sym 3 3 {- to -inf -}
 fpRndRTZ sym = wordLit sym 3 4 {- to 0    -}
-
-
-
-

src/Cryptol/Eval/Monad.hs

@@ -25,6 +25,7 @@ module Cryptol.Eval.Monad
 , delayFill
 , ready
 , blackhole
+, evalSpark
   -- * Error reporting
 , Unsupported(..)
 , EvalError(..)
@@ -33,6 +34,7 @@ module Cryptol.Eval.Monad
 , typeCannotBeDemoted
 ) where
 
+import           Control.Concurrent.Async
 import           Control.DeepSeq
 import           Control.Monad
 import qualified Control.Monad.Fail as Fail
@@ -117,6 +119,19 @@ delayFill (Thunk x) retry = Thunk $ \opts -> do
   r <- newIORef Unforced
   return $ unDelay retry r (x opts)
 
+
+-- | Begin executing the given operation in a separate thread,
+--   returning a thunk which will await the completion of
+--   the computation when forced.
+evalSpark ::
+  Eval a ->
+  Eval (Eval a)
+evalSpark (Ready x) = Ready (Ready x)
+evalSpark (Thunk x) = Thunk $ \opts ->
+  do a <- async (x opts)
+     return (Thunk $ \_ -> wait a)
+
+
 -- | Produce a thunk value which can be filled with its associated computation
 --   after the fact.  A preallocated thunk is returned, along with an operation to
 --   fill the thunk with the associated computation.

src/Cryptol/Eval/SBV.hs

@@ -39,7 +39,9 @@ import Cryptol.Eval.Type (TValue(..), finNat')
 import Cryptol.Eval.Backend
 import Cryptol.Eval.Generic
 import Cryptol.Eval.Monad
-  ( Eval(..), blackhole, delayFill, EvalError(..), Unsupported(..) )
+  ( Eval(..), blackhole, delayFill, evalSpark
+  , EvalError(..), Unsupported(..)
+  )
 import Cryptol.Eval.Value
 import Cryptol.Eval.Concrete ( integerToChar, ppBV, BV(..) )
 import Cryptol.Testing.Random( randomV )
@@ -157,6 +159,10 @@ instance Backend SBV where
     do m' <- delayFill (sbvEval m) (sbvEval retry)
        pure (pure (SBVEval m'))
 
+  sSpark _ m = SBVEval $
+    do m' <- evalSpark (sbvEval m)
+       pure (pure (SBVEval m'))
+
   sDeclareHole _ msg = SBVEval $
     do (hole, fill) <- blackhole msg
        pure (pure (SBVEval hole, \m -> SBVEval (fmap pure $ fill (sbvEval m))))
@@ -491,6 +497,8 @@ primTable  = let sym = SBV in
 
   , ("fromZ"       , fromZV sym)
 
+  , ("parmap"      , parmapV sym)
+
     -- {at,len} (fin len) => [len][8] -> at
   , ("error"       ,
       tlam $ \a ->

src/Cryptol/Eval/Value.hs

@@ -437,7 +437,7 @@ tlam f = VPoly (return . f)
 nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym
 nlam f = VNumPoly (return . f)
 
--- | A type lambda that expects a funite numeric type.
+-- | A type lambda that expects a finite numeric type.
 ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym
 ilam f = nlam (\n -> case n of
                        Nat i -> f i

src/Cryptol/Eval/What4.hs

@@ -159,6 +159,8 @@ primTable w4sym = let sym = What4 w4sym in
 
     -- Misc
 
+  , ("parmap"      , parmapV sym)
+
   , ("fromZ"       , fromZV sym)
 
     -- {at,len} (fin len) => [len][8] -> at

src/Cryptol/Eval/What4/Value.hs

@@ -30,7 +30,10 @@ import qualified What4.Utils.AbstractDomains as W4
 import Cryptol.Eval.Backend
 import Cryptol.Eval.Concrete.Value( BV(..), ppBV )
 import Cryptol.Eval.Generic
-import Cryptol.Eval.Monad (Eval(..), EvalError(..), Unsupported(..), io, delayFill, blackhole)
+import Cryptol.Eval.Monad
+   ( Eval(..), EvalError(..), Unsupported(..), io
+   , delayFill, blackhole, evalSpark
+   )
 import Cryptol.Eval.Type (TValue(..))
 import Cryptol.Eval.Value
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)
@@ -108,6 +111,10 @@ instance W4.IsExprBuilder sym => Backend (What4 sym) where
     do m' <- delayFill (w4Eval m sym) (w4Eval retry sym)
        pure (total sym (W4Eval (const m')))
 
+  sSpark _ m = W4Eval $ \sym ->
+    do m' <- evalSpark (w4Eval m sym)
+       pure (total sym (W4Eval (const m')))
+
   sDeclareHole _ msg = W4Eval $ \sym ->
     do (hole, fill) <- blackhole msg
        pure (total sym ( W4Eval (const hole), \m -> W4Eval (\sym' -> fmap (total sym') (fill (w4Eval m sym'))) ))
@@ -815,6 +822,3 @@ fpCvtToInteger sym@(What4 sy) fun r x =
             W4.RTP -> W4.realCeil sy y
             W4.RTN -> W4.realFloor sy y
             W4.RTZ -> undefined -- XXX
-
-
-