ddc-core-simpl-0.4.1.3: Disciplined Disciple Compiler code transformations.

Safe HaskellSafe-Inferred

DDC.Core.Transform.Rewrite.Disjoint

Description

Check whether two effects are non-interfering

Synopsis

Documentation

checkDisjointSource

Arguments

:: (Ord n, Show n) 
=> Type n

Type of property we want eg Disjoint e1 e2

-> RewriteEnv a n

Environment we're rewriting in.

-> Bool 

Check whether a disjointness property is true in the given rewrite environment.

Disjointness means that two effects do not interfere.

Context is important because if two regions are known to be distinct, reading from one and writing to another is valid. If they have different names they may not be distinct.

All read effects are disjoint with other reads.

 Disjoint (Read r1) (Read r2)
 Disjoint (Read r1) (DeepRead a)

Allocation effects are disjoint with everything.

 Disjoint (Alloc r) (_)

Atomic reads and write effects are disjoint if they are to distinct regions.

         Distinct r1 r2
 -----------------------------
 Disjoint (Read r1) (Write r2)

DeepWrite effects are only disjoint with allocation effects, because we don't know what regions it will write to.

An effect sum is disjoint from some other effect if all its components are.

 Disjoint f1 g /\ Disjoint f2 g
 -----------------------------
      Disjoint (f1 + f2) g

Disjointness is commutative.

 Disjoint f g
 ------------
 Disjoint g f

Example:

  checkDisjoint
    (Disjoint (Read r1 + Read r2) (Write r3))
    [Distinct r1 r3, Distinct r2 r3]
  = True

checkDistinctSource

Arguments

:: Ord n 
=> Type n

Type of the property we want, eg Distinct r1 r2

-> RewriteEnv a n

Environment we're rewriting in.

-> Bool 

Check whether a distintness property is true in the given rewrite environment.

Distinctness means that two regions do not alias.