Skip to content

Instantly share code, notes, and snippets.

@dpiponi
Created December 24, 2020 22:53
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save dpiponi/1d0acec2f80259b13287ab1dd458f885 to your computer and use it in GitHub Desktop.
Branch relaxation with monotonic time travel
Here's a block of code in some imaginary assembly language:
jmp A
block1
jmp A
block2
jmp A
block3
.A ...
If "jmp A" branches more than 127 bytes it's a 3 byte instruction, otherwise 2 bytes.
But the size of the branch instruction depends on the branch displacement which depends
on the instruction size circularly. We want a fixed point of
> {-# LANGUAGE ApplicativeDo #-}
> import Control.Applicative
> import Data.Function
> infixr :<
> assemble7 :: (Bool, Bool, Bool) -> (Bool, Bool, Bool)
> assemble7 (shortJump1, shortJump2, shortJump3) =
> let jmpSize1 = if shortJump1 then 2 else 3
> jmpSize2 = if shortJump2 then 2 else 3
> jmpSize3 = if shortJump3 then 2 else 3
> shortJump1' = jmpSize1 + blockSize1 + jmpSize2 + blockSize2 + jmpSize3 + blockSize3 < 128
> shortJump2' = jmpSize2 + blockSize2 + jmpSize3 + blockSize3 < 128
> shortJump3' = jmpSize3 + blockSize3 < 128
> blockSize1 = 64
> blockSize2 = 30
> blockSize3 = 28
> in (shortJump1', shortJump2', shortJump3')
Sometimes this might cause non-termination. How can we impose a policy on the programmer to make sure
this never happens?
Note that `shortJump[123]` are effectively forward references. If we use `fix` on `assemble7` then
it basically picks up the values generated on the previous iteration. One way to ensure convergence
is to impose this condition: all forward references are going to go through an operator `box` which
actually computes the minimum (considering `Bool` as an instance of `Ord`) value of its argument seen
on any iteration, starting optimistically with `True`. Because all forward references go through
a monotonic function like this we're guaranteed convergence. There are a few ways of doing this but
I'm going to replace our logical variables with streams:
> data Stream a = a :< Stream a deriving Show
> instance Functor Stream where
> fmap f (x :< xs) = f x :< fmap f xs
> instance Applicative Stream where
> pure x = x :< pure x
> liftA2 f (x :< xs) (y :< ys) = f x y :< liftA2 f xs ys
> assemble longJump =
> let branchLocation = 0
> codeLength = 125 + if longJump then 3 else 2
> destination = branchLocation + codeLength
> in destination - branchLocation > 127
> streamScanl :: (a -> b -> a) -> a -> Stream b -> Stream a
> streamScanl f a ~(x :< xs) = a :< streamScanl f (f a x) xs
> streamHead (a :< _) = a
> streamTake 0 _ = []
> streamTake n (x :< xs) = x : streamTake (n - 1) xs
Here is `box` doing a delay of 1 and computing the "cumulative" min:
> box :: Stream Bool -> Stream Bool
> box = streamScanl (&&) True
Sorry it's ugly, I couldn't get `ApplicativeDo` to do this. I hope you see that
conceptually it's `assemble7` "lifted" to streams.
> assemble8 :: Stream (Bool, Bool, Bool) -> Stream (Bool, Bool, Bool)
> assemble8 shortJumps =
> let shortJump1 = (\(a, _, _) -> a) <$> shortJumps
> shortJump2 = (\(_, b, _) -> b) <$> shortJumps
> shortJump3 = (\(_, _, c) -> c) <$> shortJumps
> jmpSize1 = (\s -> if s then 2 else 3) <$> box shortJump1
> jmpSize2 = (\s -> if s then 2 else 3) <$> box shortJump2
> jmpSize3 = (\s -> if s then 2 else 3) <$> box shortJump3
The crucial thing to note here is that we'd prefer `shortJump[123]'` to be `True` but we can accept both `False` and
`True` so this code is compatible with `box`:
> shortJump1' = (\j1 j2 j3 -> j1 + blockSize1 + j2 + blockSize2 + j3 + blockSize3 < 128) <$> jmpSize1 <*> jmpSize2 <*> jmpSize3
> shortJump2' = (\j2 j3 -> j2 + blockSize2 + j3 + blockSize3 < 128) <$> jmpSize2 <*> jmpSize3
> shortJump3' = (\j3 -> j3 + blockSize3 < 128) <$> jmpSize3
> blockSize1 = 64
> blockSize2 = 30
> blockSize3 = 30
> in (\a b c -> (a, b, c)) <$> shortJump1' <*> shortJump2' <*> shortJump3'
Now we walk our stream until we find convergence:
> solve :: (Eq a) => (Stream a -> Stream a) -> a
> solve f =
> let findEqual (x :< y :< ys) | x == y = x
> findEqual (x :< xs) = findEqual xs
> in findEqual (fix f)
This example is trivial and converges in one step
> main = do
> print $ solve assemble8
Anyway, this is a convoluted way of doing all this. But here's my main point: there's a logic lurking here. Consider
code like
f (a, b, c) =
let a' = a || b || c
b' = a || c
c' = not a && not b
in (a', b', c')
A fixed point solves a system of logical equations
a = a ∨ b ∧ c
b = a ∧ c
c = ¬ a ∧ ¬ b
Now introduce boxes. I'm too lazy to lift by hand so here's unlifted pseudocode:
f (a, b, c) =
let a' = box (a || b || c)
b' = box (a || c)
c' = box (not a && not b)
in (a', b', c')
We're solving equations like:
a = □ (a ∨ b ∧ c)
b = □ (a ∨ c)
c = □ (¬ a ∧ ¬ b)
But what does □ mean in a purely logical context?
Well, I'm pretty sure □ is the modal operator from provability logic (GL).
See https://arxiv.org/abs/1401.4002 for one angle on this.
See my own blog post http://blog.sigfpe.com/2017/07/self-referential-logic-via-self.html for another.
(That post also gives examples that take longer to converge.)
The stream interpretation is (disguised) in Boolos' book on Provability Logic.
So my claim is this: provability logic is the logic of convergent monotonic time
travel à la @ezyang as suggested here: https://twitter.com/ezyang/status/1341946859053608961
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment