Portability | portable |
---|---|

Stability | experimental |

Maintainer | erkokl@gmail.com |

The PrefixSum algorithm over power-lists and proof of the Ladner-Fischer implementation. See http://www.cs.utexas.edu/users/psp/powerlist.pdf and http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.

- type PowerList a = [a]
- tiePL :: PowerList a -> PowerList a -> PowerList a
- zipPL :: PowerList a -> PowerList a -> PowerList a
- unzipPL :: PowerList a -> (PowerList a, PowerList a)
- ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
- lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
- flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
- thm1 :: IO ThmResult
- thm2 :: IO ThmResult
- thm3 :: IO ThmResult
- genPrefixSumInstance :: Int -> Symbolic SBool
- prefixSum :: Int -> IO ThmResult
- ladnerFischerTrace :: Int -> IO ()
- scanlTrace :: Int -> IO ()

# Formalizing power-lists

A poor man's representation of powerlists and basic operations on them: http://www.cs.utexas.edu/users/psp/powerlist.pdf. We merely represent power-lists by ordinary lists.

zipPL :: PowerList a -> PowerList a -> PowerList aSource

The zip operator, zips the power-lists of the same size, returns a powerlist of double the size.

# Reference prefix-sum implementation

ps :: (a, a -> a -> a) -> PowerList a -> PowerList aSource

Reference prefix sum (`ps`

) is simply Haskell's `scanl1`

function.

# The Ladner-Fischer parallel version

lf :: (a, a -> a -> a) -> PowerList a -> PowerList aSource

The Ladner-Fischer (`lf`

) implementation of prefix-sum. See http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf
or pg. 16 of http://www.cs.utexas.edu/users/psp/powerlist.pdf.

# Sample proofs for concrete operators

flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBoolSource

Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element.

Proves Ladner-Fischer is equivalent to reference specification for addition.
`0`

is the left-unit element, and we use a power-list of size `8`

.

Proves Ladner-Fischer is equivalent to reference specification for the function `max`

.
`0`

is the left-unit element, and we use a power-list of size `16`

.

# Attempt at proving for arbitrary operators

Try proving correctness for an arbitrary operator. This proof will *not* go through since the
SMT solver does not know that the operator associative and has the given left-unit element. We have:

`>>>`

Falsifiable. Counter-example: s0 = 0 :: SWord32 s1 = 0 :: SWord32 s2 = 0 :: SWord32 s3 = 0 :: SWord32 s4 = 0 :: SWord32 s5 = 0 :: SWord32 s6 = 0 :: SWord32 s7 = 3221225472 :: SWord32 -- uninterpreted: u u = 0 -- uninterpreted: flOp flOp 0 3221225472 = 2147483648 flOp 0 2147483648 = 3758096384 flOp _ _ = 0`thm3`

You can verify that the above function for `flOp`

is not associative:

ghci> flOp 3221225472 (flOp 2147483648 3221225472) 0 ghci> flOp (flOp 3221225472 2147483648) 3221225472 2147483648

Also, the unit `0`

is clearly not a left-unit for `flOp`

, as the third
equation for `flOp`

will simply map many elements to `0`

.

# Proving for arbitrary operators using axioms

genPrefixSumInstance :: Int -> Symbolic SBoolSource

Generate an instance of the prefix-sum problem for an arbitrary operator, by telling the SMT solver the necessary axioms for associativity and left-unit. The first argument states how wide the power list should be.

prefixSum :: Int -> IO ThmResultSource

Prove the generic problem for powerlists of given sizes. Note that this will only work for Yices-1. This is due to the fact that Yices-2 follows the SMT-Lib standard and does not accept bit-vector problems with quantified axioms in them, while Yices-1 did allow for that. The crux of the problem is that there are no SMT-Lib logics that combine BV's and quantifiers, see: http://goedel.cs.uiowa.edu/smtlib/logics.html. So we are stuck until new powerful logics are added to SMT-Lib.

Here, we explicitly tell SBV to use Yices-1 that did not have that limitation. Tweak the executable location accordingly below for your platform..

We have:

`>>>`

Q.E.D.`prefixSum 2`

`>>>`

Q.E.D.`prefixSum 4`

Note that these proofs tend to run long. Also, Yices ran out of memory
and crashed on my box when I tried for size `8`

, after running for about 2.5 minutes..

# Inspecting symbolic traces

ladnerFischerTrace :: Int -> IO ()Source

A symbolic trace can help illustrate the action of Ladner-Fischer. This generator produces the actions of Ladner-Fischer for addition, showing how the computation proceeds:

`>>>`

INPUTS s0 :: SWord8 s1 :: SWord8 s2 :: SWord8 s3 :: SWord8 s4 :: SWord8 s5 :: SWord8 s6 :: SWord8 s7 :: SWord8 CONSTANTS s_2 = False s_1 = True TABLES ARRAYS UNINTERPRETED CONSTANTS USER GIVEN CODE SEGMENTS AXIOMS DEFINE s8 :: SWord8 = s0 + s1 s9 :: SWord8 = s2 + s8 s10 :: SWord8 = s2 + s3 s11 :: SWord8 = s8 + s10 s12 :: SWord8 = s4 + s11 s13 :: SWord8 = s4 + s5 s14 :: SWord8 = s11 + s13 s15 :: SWord8 = s6 + s14 s16 :: SWord8 = s6 + s7 s17 :: SWord8 = s13 + s16 s18 :: SWord8 = s11 + s17 CONSTRAINTS OUTPUTS s0 s8 s9 s11 s12 s14 s15 s18`ladnerFischerTrace 8`

scanlTrace :: Int -> IO ()Source

Trace generator for the reference spec. It clearly demonstrates that the reference implementation fewer operations, but is not parallelizable at all:

`>>>`

INPUTS s0 :: SWord8 s1 :: SWord8 s2 :: SWord8 s3 :: SWord8 s4 :: SWord8 s5 :: SWord8 s6 :: SWord8 s7 :: SWord8 CONSTANTS s_2 = False s_1 = True TABLES ARRAYS UNINTERPRETED CONSTANTS USER GIVEN CODE SEGMENTS AXIOMS DEFINE s8 :: SWord8 = s0 + s1 s9 :: SWord8 = s2 + s8 s10 :: SWord8 = s3 + s9 s11 :: SWord8 = s4 + s10 s12 :: SWord8 = s5 + s11 s13 :: SWord8 = s6 + s12 s14 :: SWord8 = s7 + s13 CONSTRAINTS OUTPUTS s0 s8 s9 s10 s11 s12 s13 s14`scanlTrace 8`