Parallel and sequential circuits

And the relation between them

In Agda

  • Last talk was more of an overview
  • Today we show some examples
    • Some "circuit patterns"
    • Parallel and sequential
    • Lots of pictures, lots of Agda ☺

What does this compute?

Haskell's mapAccumL


mapAccumL :: (s -> a -> (s,b)) -> s -> [a] -> (s, [b])
mapAccumL _ s []     = (s, [])
mapAccumL f s (x:xs) = (s″,y:ys)
                       where (s′, y ) = f s x
                             (s″,ys) = mapAccumL f s′ xs
						

mapAccL in Agda (λ₁)


mapAccL : ∀ n (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (s : λ₁ σ) (xs : λ₁ (vec ρ n))
			→ λ₁ (σ ⊗ vec τ n)
mapAccL zero     _ s _  = s , []
mapAccL (suc n′) f s xs = case[] xs of λ x xs′ →
                            case⊗ (f s x) of λ s′ y →
                              case⊗ (mapAccL n′ f s′ xs′) of λ s″ ys′ →
                                s″ , (y ∷ ys′)
						

Definitions and notation

  • Universe of types for circuit I/O
    • Unit, base type, sums, products
    • Notation for object type vars: σₙ, τₙ, ρₙ

data Uₚ (B : Set) : Set where
  𝟙     : Uₚ B
  ι     : Uₚ B
  _⊗_   : (τ₁ τ₂ : Uₚ B) → Uₚ B
  _⊕_   : (τ₁ τ₂ : Uₚ B) → Uₚ B

Tₚ : ∀ {B} (τ : Uₚ B) → Set
Tₚ      𝟙          = ⊤
Tₚ {B}  ι          = B
Tₚ      (τ₁ ⊗ τ₂)  = Tₚ τ₁  × Tₚ τ₂
Tₚ      (τ₁ ⊕ τ₂)  = Tₚ τ₁  ⊎ Tₚ τ₂
						

Context, Environments and Gates

  • A Ctxt is a list of Uₚ
  • An Env is a heterogenous list indexed by a Ctxt
    • Contexts: Γₙ, Δₙ,…
    • Environments: γₙ, δₙ,…
  • A Gate has an interface (Δ,τ) and a spec (⟦–⟧g)

record Gate {B} (Δ : Ctxt B) (τ : Uₚ B) : Set where
  constructor MkG
  field  ⟦–⟧g : Env Tₚ Δ → Tₚ τ

ONE : ∀ {B} → Gate {B} ε 𝟙
ONE = MkG constOne
  where  constOne : ∀ {B} (γ : Env {B} Tₚ ε) → Tₚ {⊤} 𝟙
         constOne = const tt
						

The "Lambda1" EDSL

  • Core datatype (λ₁′) indexed by inputs, output
  • De Bruijn indices, let's for sharing, explicit looping construct
    • Products, sums, fundamental gates
    • No arrow types: no lambda, no application

data λ₁′ {B} : (Γ : Ctxt B) (τ : Uₚ B) → Set where
  [_]    : ∀ {Γ τ}                (i : Γ ∋ τ)
                                   → λ₁′ Γ τ

  letₓ′  : ∀ {Γ σ τ}    (x : λ₁′ Γ σ)  (b : λ₁′ (σ ◅ Γ) τ)
                                   → λ₁′ Γ τ

  loop′  : ∀ {Γ σ τ}       (c : λ₁′ (σ ◅ Γ) (σ ⊗ τ))
                                  → λ₁′ Γ τ
						

Lambda1 surface language

  • De Bruijn isn't so friendly
    • So we transform Agda binders into binders of the EDSL
    • Using the "unembedding" technique by Lindley et al., plus syntax

λ₁ : ∀ {B} (τ : Uₚ B) → Set
λ₁ {B} τ = ∀ {Γ : Ctxt B} → λ₁′ Γ τ

letₓ : ∀ {B} {σ τ} (x : λ₁ σ) (f : λ₁ σ → λ₁ τ) → λ₁ {B} τ
syntax letₓ eₓ (λ x → b) = let͘ x ≔ eₓ in͘ b

loop : ∀ {B} {σ τ} (f : λ₁ σ → λ₁ (σ ⊗ τ)) → λ₁ {B} τ
syntax loop {σ = σ} (λ s → b) = loop s ∶ σ in͘ b

fork : ∀ {B} {τ} (x : λ₁ τ) → λ₁ {B} (τ ⊗ τ)
fork x = let͘ y ≔ x in͘ (y , y)
						

Back to examples for a while

  • Remember mapAccL

Sequential mapAccL

  • We can easily define a sequential version of mapAccL
  • In mapAccL-seq, there's a loop instead of recursion
  • But what does the delay mean?

Semantics, one step at a time

  • Loops mean circuits can have state
    • Semantics in the state monad
  • There's an inductive family giving the state type of a circuit

⟦_⟧s : (c : λ₁′ Γ τ) (s : λₛ c) (γ : Env Tₚ Γ) → (λₛ c × Tₚ τ)
						

data λₛ {B} : {Γ : Ctxt B} {τ : Uₚ B} (c : λ₁′ Γ τ) → Set where
  [_]ₛ   : ∀ {Γ σ}     (i : Γ ∋ σ)                            → λₛ [ i ]
  letₛ   : ∀ {Γ σ τ}   {x : λ₁′ Γ σ} {e : λ₁′ (σ ◅ Γ) τ}  (xₛ : λₛ x) (eₛ : λₛ e)
                                                            → λₛ (letₓ′ x e)

  loopₛ  : ∀ {Γ σ τ}   {c : λ₁′ (σ ◅ Γ) (σ ⊗ τ)}         (iₛ : Tₚ σ) (cₛ : λₛ c)
                                                            → λₛ (loop′ c)

  _,ₛ_   : ∀ {Γ τ₁ τ₂}  {x : λ₁′ Γ τ₁} {y : λ₁′ Γ τ₂}        (xₛ : λₛ x) (yₛ : λₛ y)
                                                              → λₛ (x ,′ y)
						

Circuits in (discrete) time: n steps

  • One state transition per clock cycle
  • We can simulate a number of cycles with ⟦_⟧n
    • Final state is exposed
    • Usefulness clear soon

⟦_⟧n : (c : λ₁′ Γ τ) (s : λₛ c) (γn : Vec (Env Tₚ Γ) n) → λₛ c × Vec (Tₚ τ) n
⟦_⟧n n c s = mapAccumL n s ⟦ c ⟧s
						

Parallel vs. sequential

  • Now it's almost obvious how mapAccL and mapAccL are related
  • In one step from mapAccL, in n steps from mapAccL-seq
  • But the exact relation is not so short…

mapAccL-seq : (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (x : λ₁ ρ) → λ₁ τ
mapAccL-seq {σ} f x = loop s ∶ σ in f s x
						

Par. vs. seq.: mapAccL vs. mapAccL-seq


_⊒_ : ∀ {α β φ : Set} → φ × (α × β) → α × β → Set
(_ , sa,ra) ⊒ sb,rb = sa,ra ≡ sb,rb
						

n : ℕ
X : λₛ (mapAccL n f)

σ ρ τ : Uₚ
f     : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)
s     : Tₚ σ
xs    : Tₚ (vec ρ n)

MALSt  : Tₚ σ → λₛ (mapAccL-seq {σ} f)
MALIns : Tₚ (vec ρ n) → Vec (Env Tₚ (ρ ◅ ε)) n

⟦ mapAccL n f ⟧s X (↦ s ◅ ↦ xs ◅ ε) ⊒ ⟦ mapAccL-seq f ⟧n n (MALSt s) (MALIns xs)
						

From mapAccL, lots of others…


iterate : ∀ n (f : λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ (vec τ (suc n))
iterate n {τ} f x = mapAccL n f′ x (replicate unit)
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)
							

Sequential version: iterate-seq


iterate-seq : (f : λ₁ τ → λ₁ τ) → λ₁ τ
iterate-seq {τ} f = mapAccL-seq f′ unit
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)
							

If intermediate results don't matter: repeat


	repeat : ∀ n (f : λ₁ τ → λ₁ τ) → λ₁ τ
	repeat n f x  = fst (iterate n f x)
							

repeat-seq is a little interesting

  • We say that intermediate results don't matter
  • So the output stream elements from y₀ to yₙ₋₁ don't matter
    • We only require that yₙ = fⁿ(x)
  • In particular, they can be the intermediate results…

repeat : (f : λ₁ τ → λ₁ τ) → λ₁ τ
repeat-seq = iterate-seq
						

proj₂ (⟦ repeat n f ⟧s X (↦ x ◅ ε)) ≡ proj₁ (⟦ repeat-seq f ⟧n n (repSt x)  emptys)
						

Folds and scans, all-in-one

Definitions: foldl×scanl, foldl, scanl


foldl×scanl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n))
              → λ₁ (τ ⊗ vec τ (suc n))
foldl×scanl zero     _⊞_ e _  = e , (e ∷ [])
foldl×scanl (suc n′) _⊞_ e xs = case⊗ mapAccL (suc n′) f′ e xs of λ fold sums′ →
                                  fold , (e ∷ sums′)
  where f′ : λ₁ τ → λ₁ τ → λ₁ (τ ⊗ τ)
        f′ acc x = fork (acc ⊞ x)
							

foldl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n)) → λ₁ τ
foldl n _⊞_ e = fst (foldl×scanl n _⊞_ e)
							

scanl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n))
        → λ₁ (vec τ (suc n))
scanl n _⊞_ e xs = snd (foldl×scanl n _⊞_ e)
							

Sequential version: foldl×scanl

  • Interesting extra "shift": extra value in front of the stream

scanl-seq : (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ τ
scanl-seq _⊞_ x = comp (mapAccL-seq f′ x) shift
  where  f′ : λ₁ τ → λ₁ τ → λ₁ (τ ⊗ τ)
         f′ acc x = fork (acc ⊞ x)
							

Composition and pipelining

  • Pardon the flipped composition, it makes things easier…

comp : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
comp = flip _∘_
							

compD : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
compD f g = comp (comp f shift) g
							

Correctness of pipelining

  • Here the whole output Stream really matters
  • The pipelined version should be shifted by one time unit

⟦ comp f g ⟧* (stComp sf sg) γ ≈ tail (⟦ compD f g ⟧* (stCompD sf sg sd) γ)
							

N-ary composition

  • Type-aligned sequence: VecA F as bs
    • fs : VecA F as bs = [f₀ : F a₀ b₀, f₁ : F a₁ b₁, …

compN : let F = λ σ τ → (λ₁ σ → λ₁ τ)
        in (fs : VecA F σs τs) → λ₁ (head σs) → λ₁ (last τs))
compN (f ∷ fs′) = comp …
						

⟦ compN fs ⟧* (stCompN n sf) γ ≈ drop n (⟦ compDN fs ⟧* (stCompDN n sf sd) γ)
						

That's all for today!