parmap <<loop>>

[weaversa]

Treemap : [15][32]
Treemap = tail T
  where
    T = [undefined] # branches # leaves
    branches = map (\[x, y] -> x + y) (tail (split T))
    leaves   = [ 0 .. 7 ]

Treeparmap : [15][32]
Treeparmap = tail T
  where
    T = [undefined] # branches # leaves
    branches = parmap (\[x, y] -> x + y) (tail (split T))
    leaves   = [ 0 .. 7 ]

Test> Treemap
[28, 6, 22, 1, 5, 9, 13, 0, 1, 2, 3, 4, 5, 6, 7]
Test> Treeparmap
<<loop>>

[robdockins]

Parmap is deliberately stricter than it "should" be. This is to ensure that useful work is actually done in the spawned threads. Otherwise, you are very likely to spawn off a bunch of threads that do very little work to construct a thunk which is then later forced in the main thread, accidentally re-sequentializing your computation. As a result, you'll have to be a lot more careful about evaluation order. In particular, you probably shouldn't use it in a recursive definition like this.

[weaversa]

Here is a "more careful" version. I think it's gonna be a challenge to generalize :-)

  Treeparmap : [15][32]
  Treeparmap = T
    where
      T = branches1 # branches2 # branches4 # leaves
      branches1 = parmap (\[x, y] -> x + y) (groupBy`{2} branches2) : [1][32]
      branches2 = parmap (\[x, y] -> x + y) (groupBy`{2} branches4) : [2][32]
      branches4 = parmap (\[x, y] -> x + y) (groupBy`{2} leaves)    : [4][32]
      leaves   = [ 0 .. 7 ]                                         : [8][32]

[robdockins]

Yeah, it's a bit tricky. But, I think you can use function recursion instead of value recursion to do this sort of thing. Function recursion doesn't cause the subterm sharing that you find in the stream recurrence style (which is why we usually recommend against it). Let me see if I can come up with a version that demonstrates what I mean.

[robdockins]

The trickiest part here is actually explaining to Cryptol how the power of 2 sequence goes. If you just wanted the final answer instead of the sequence, I think you'd have an easier time. Anyway, here's what I have for now.

Treeparmap : [15][32]
Treeparmap = q.1
  where
  q = step (step (step (leaves, leaves)))
  leaves = [ 0 .. 7 ]

step : {n, m} fin n => ([2*n][32],[m][32]) -> ([n][32], [n+m][32])
step (xs,zs) = (ys, ys#zs)
  where ys = combineBy (+) xs

combineBy : {n, a} fin n => (a -> a -> a) -> [2*n]a -> [n]a
combineBy op xs = parmap f (groupBy`{2} xs)
  where f [x, y] = op x y

[robdockins]

Here's one that just computes the final sum. Wouldn't be hard to generalize to splitting factors other than 2, I think.

combineBy : {n, a} fin n => (a -> a -> a) -> [2*n]a -> [n]a
combineBy op xs = parmap f (groupBy`{2} xs)
  where f [x, y] = op x y

Treeparmap' : {n} (fin n, n >= 1) => [n][32] -> [32]
Treeparmap' xs = if `n == 1 then xs@0 else Treeparmap'`{n%2 + n/2} (hd#tl')
  where
  (hd,tl) = splitAt`{ n%2 } xs
  tl' = combineBy (+) tl

[robdockins]

Another variation:

Treeparmap'' : {n} (fin n, n >= 1) => [n][32] -> [inf][32] -> [inf][32]
Treeparmap'' xs res = if `n == 1 then xs#res else Treeparmap''`{n%2 + n/2} (hd#tl') (xs#res)
  where
  (hd,tl) = splitAt`{ n%2 } xs
  tl' = combineBy (+) tl

Main> take`{2^^4 - 1} (Treeparmap'' [ 0 .. 7 ] zero)
[28, 6, 22, 1, 5, 9, 13, 0, 1, 2, 3, 4, 5, 6, 7]

[weaversa]

I was considering the [inf] trick myself 👍

Treeparmap : {n, a} (fin n, n >= 1) => ([2]a -> a) -> [2^^n]a -> [2 * (2^^n) - 1]a
Treeparmap f leaves = take (Treeparmap'`{n=1} `(2^^(n-1)) f leaves')
  where leaves' = leaves # leaves'

Treeparmap' : {n, a} (fin n, n >= 1) => Integer -> ([2]a -> a) -> [inf]a -> [inf]a
Treeparmap' nmax f leaves = branches # leaves'
  where
    branches = parmap f (take`{n} (groupBy`{2} leaves'))
    leaves'  = if `n == nmax then leaves
               else Treeparmap'`{n*2} nmax f leaves

Main> Treeparmap (\[a, b] -> a + b) [0..7]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
[28, 6, 22, 1, 5, 9, 13, 0, 1, 2, 3, 4, 5, 6, 7]

[weaversa]

If the deliberate restriction is removed, does the first example go through and make use of the parallel features?

[weaversa]

Here I'm laying in some node specific values (so I can multiply node weights), and if trace is left in, there are no problems. Otherwise, there is a <<loop>>

Treeparmap : {n, a, b} (fin n, n >= 1) => (([2]a, b) -> a) -> [2^^n]a -> [2^^n-1]b -> [2 * (2^^n) - 1]a
Treeparmap f leaves nodeinfo = take (Treeparmap'`{n=1} `(2^^(n-1)) f leaves' nodeinfo')
  where
    leaves'   = leaves # leaves'
    nodeinfo' = nodeinfo # nodeinfo'

Treeparmap' : {n, a, b} (fin n, n >= 1) => Integer -> (([2]a, b) -> a) -> [inf]a -> [inf]b -> [inf]a
Treeparmap' nmax f leaves nodeinfo = branches # leaves'
  where
    branches = trace "branches" (`n, take`{n} (zip (groupBy`{2} leaves') nodeinfo))
               (parmap f (take`{n} (zip (groupBy`{2} leaves') nodeinfo)))
    leaves'  = if `n == nmax then leaves
               else Treeparmap'`{n*2} nmax f leaves (drop`{n} nodeinfo)

With trace

Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])
branches (1, [([68, 245], 1)])
[313, 68, 245, 2, 15, 36, 13, 0, 1, 2, 3, 4, 5, 6, 7]

Without trace:

Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member

<<loop>>

It feels like trace is forcing the previous level of parmap results to resolve, acting as blocker (similar to a mutex?) before allowing the next parmap to start up.

[weaversa]

Now I'm getting inconsistent behavior! Every run can give a <<loop>> or not, and at different times.

Treeparmap : {n, a, b} (fin n, n >= 1) => (([2]a, b) -> a) -> [2^^n]a -> [2^^n-1]b -> [2 * (2^^n) - 1]a
Treeparmap f leaves nodeinfo = take (Treeparmap'`{n=1} `(2^^(n-1)) f leaves' nodeinfo')
  where
    leaves'   = leaves # leaves'
    nodeinfo' = nodeinfo # nodeinfo'

Treeparmap' : {n, a, b} (fin n, n >= 1) => Integer -> (([2]a, b) -> a) -> [inf]a -> [inf]b -> [inf]a
Treeparmap' nmax f leaves nodeinfo = branches # leaves'
  where
    branches = trace "branches" (`n, zip (take`{n} (groupBy`{2} leaves')) nodeinfo')
               (parmap f (zip (take`{n} (groupBy`{2} leaves')) nodeinfo'))
    leaves'  = if `n == nmax then leaves
               else Treeparmap'`{n*2} nmax f leaves nodeinfo''
    (nodeinfo' # nodeinfo'') = nodeinfo

Here I enter the same command over and over again --

Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])

<<loop>> while evaluating (at Cryptol:1080:5--1080:7, xs)
Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])
branches (1, [([68, 245], 1)])
[313, 68, 245, 2, 15, 36, 13, 0, 1, 2, 3, 4, 5, 6, 7]
Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])

<<loop>> while evaluating (at Cryptol:1080:5--1080:7, xs)
Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])
branches (1, [([68, 245], 1)])
[313, 68, 245, 2, 15, 36, 13, 0, 1, 2, 3, 4, 5, 6, 7]
Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])

<<loop>> while evaluating (at Cryptol:1080:5--1080:7, xs)
Main> Treeparmap (\([a, b], c) -> (a + b) * c) [0..7] [1, 4, 5, 2, 3, 4, 1]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of sequence member
branches (4, [([0, 1], 2), ([2, 3], 3), ([4, 5], 4), ([6, 7], 1)])
branches (2, [([2, 15], 4), ([36, 13], 5)])
branches (1, [([68, 245], 1)])
[313, 68, 245, 2, 15, 36, 13, 0, 1, 2, 3, 4, 5, 6, 7]

[weaversa]

Hopefully this is an opportunity to see what action trace is performing that causes the <<loop>> to be avoided, and force that action to happen right before loops are checked for...or maybe right before parmap finishes...? maybe? something like that?

[robdockins]

Trace is another operation that is in some sense "too strict" because it has to evaluate the term to print it. It behaves a bit like Haskell's magic seq primitive. You can achieve largely the same effect with the following trick:

deepseq : {a, b} (Eq a) => a -> b -> b
deepseq x y = assert (x == x) "impossible" y

Treeparmap : {n, a, b} (Eq a, fin n, n >= 1) => (([2]a, b) -> a) -> [2^^n]a -> [2^^n-1]b -> [2 * (2^^n) - 1]a
Treeparmap f leaves nodeinfo = take (Treeparmap'`{n=1} `(2^^(n-1)) f leaves' nodeinfo')
  where
    leaves'   = leaves # leaves'
    nodeinfo' = nodeinfo # nodeinfo'

Treeparmap' : {n, a, b} (Eq a, fin n, n >= 1) => Integer -> (([2]a, b) -> a) -> [inf]a -> [inf]b -> [inf]a
Treeparmap' nmax f leaves nodeinfo = branches # leaves'
  where
    branches = deepseq (leaves'@0) (parmap f (take`{n} (zip (groupBy`{2} leaves') nodeinfo)))
    leaves'  = if `n == nmax then leaves
               else Treeparmap'`{n*2} nmax f leaves (drop`{n} nodeinfo)

With multiple cores enabled, I'm seeing the same inconsistent results you report.

Ultimately, I think the problem is that parmap exposes a race condition in the thunk lifetime, which is why you're getting inconsistent results. If the thunks happen to be forced and evaluated in data-dependency order, everything works out. Otherwise, you get problems. I have some ideas about how to improve this, but it's not going to be a simple fix.

[weaversa]

I still don’t see why my Treeparmap with the extra node info causes loops when the Treeparmap without doesn’t. It is finicky huh?

[weaversa]

Oh...I see...the version w/out trace does occasionally work (I tried about 40 times before one worked). I feel like you probably already knew that...

Main> Treeparmap (\([a, b], c) -> a + b + c) [0..7] [0..6]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'

<<loop>> while evaluating (at test.cry:12:5--12:12, Main::leaves')
Main> Treeparmap (\([a, b], c) -> a + b + c) [0..7] [0..6]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
[49, 14, 35, 4, 9, 14, 19, 0, 1, 2, 3, 4, 5, 6, 7]

[weaversa]

Trying the depseq version on large trees, parmap seems to perform the same as replacing parmap with map. Though, again...maybe you already knew that.