Causally consistent dynamic slicing
Roly Perera1,2 , Deepak Garg3 , and James Cheney1
1

Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, UK
rperera@inf.ed.ac.uk, jcheney@inf.ed.ac.uk

2

School of Computing Science, University of Glasgow, Glasgow, UK
roly.perera@glasgow.ac.uk

3

Max Planck Institute for Software Systems, Saarbrücken, Germany
dg@mpi-sws.org

arXiv:1610.02327v1 [] 7 Oct 2016

Abstract
We offer a lattice-theoretic account of dynamic slicing for π-calculus, building on prior work in the
sequential setting. For any run of a concurrent program, we exhibit a Galois connection relating
forward slices of the start configuration to backward slices of the end configuration. We prove
that, up to lattice isomorphism, the same Galois connection arises for any causally equivalent
execution, allowing an efficient concurrent implementation of slicing via a standard interleaving
semantics. Our approach has been formalised in the dependently-typed language Agda.
1998 ACM Subject Classification D.1.3 Concurrent Programming; D.2.5 Testing and debugging
Keywords and phrases π-calculus; dynamic slicing; causal equivalence; Galois connection
Digital Object Identifier 10.4230/LIPIcs.CONCUR.2016.18

1

Introduction

Dynamic slicing, due originally to Weiser [18], is a runtime analysis technique with applications
in debugging, security and provenance tracking. The basic goal is to identify a sub-program,
or program slice, that may affect an outcome of interest called the slicing criterion, such as
the value of a variable. Dynamic slicing in concurrent settings is often represented as a graph
reachability problem, thanks to influential work by Cheng [2]. However, most prior work
on dynamic slicing for concurrency does not yield minimum slices, nor allows particularly
flexible slicing criteria, such as arbitrary parts of configurations. Systems work on concurrent
slicing [8, 13, 17] tends to be largely informal.
Perera et al [14] developed an approach where backward dynamic slicing is treated as a
kind of (abstract) reverse execution or “rewind” and forward slicing as a kind of (abstract)
re-execution or “replay”. Forward and backward slices are related by a Galois connection,
ensuring the existence of minimal slices. This idea is straightforward in the sequential setting
of the earlier work. However, generalising it to concurrent programs is non-trivial. Suppose
we run a concurrent computation, discover a bug, and then wish to compute a dynamic slice.
It would clearly be impractical to require the slice be computed using the exact interleaving
of the original run, particularly in a distributed setting. On the other hand, computing the
slice using a brand-new concurrent execution may make different non-deterministic choices,
producing a slice of a computation other than the one intended.
Intuitively, any execution which exhibits the same causal structure should be adequate for
computing the slice, and any practical approach to concurrent slicing should take advantage
of this. Danos and Krivine [4] make a similar observation about reversible concurrency,
arguing that the most liberal notion of reversibility is one that just respects causality: an
action can only be undone after all the actions that causally depend on it have been undone.
© Roly Perera, Deepak Garg and James Cheney;
licensed under Creative Commons License CC-BY
27th International Conference on Concurrency Theory (CONCUR 2016).
Editors: Josée Desharnais and Radha Jagadeesan; Article No. 18; pp. 18:1–18:14
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

18:2

Causally consistent dynamic slicing

Scheduler thread 1
−−−→
−−−→
−−−→
−−−→
−−−→

a1 .c1 .(b1 .c2 .r1 + c2 .b1 .r1 )
c1 .(b1 .c2 .r1 + c2 .b1 .r1 )
b1 .c2 .r1 + c2 .b1 .r1
b1 .c2 .r1 + c2 .b1 .r1
c2 .r1
a1 .c1 .(b1 .c2 .r1 + c2 .b1 .r1 )

A1

Scheduler thread 2
|
|
|
|
|
|

c1 .a2 .c2 .(b2 .c1 .r2 + c1 .b2 .r2 )
c1 .a2 .c2 .(b2 .c1 .r2 + c1 .b2 .r2 )
a2 .c2 .(b2 .c1 .r2 + c1 .b2 .r2 )
c2 .(b2 .c1 .r2 + c1 .b2 .r2 )
c2 .(b2 .c1 .r2 + c1 .b2 .r2 )
b2 .c1 .r2 + c1 .b2 .r2

|
|
|
|
|
|

a1 .b1 .p1
b1 .p1
b1 .p1
b1 .p1
b1 .p1
b1 .p1

A2
|
|
|
|
|
|

a2 .b1 .p2
a2 .b1 .p2
a2 .b1 .p2
b1 .p2
a2 .b1 .p2
a2 .b1 .p2

..............................................................................................................................................
Figure 1 Stuck configuration, overlaid with backward slice with respect to final state of thread 1

In this paper we formalise dynamic slicing for π-calculus, and show that any causally equivalent execution generates precisely the same slicing information. We do this by formalising
slicing with respect to a particular execution t̃, and then proving that slicing with respect to
any causally equivalent computation ũ yields the same slice, after a unique “rewiring” which
interprets the path witnessing t̃ ' ũ as a lattice isomorphism relating the two slices. The
isomorphism is constructive, rewriting one slice into the other: this allows non-deterministic
metadata (e.g. memory addresses or transaction ids) in the slicing execution to be aligned
with the corresponding metadata in the original run. We build on an earlier “proof-relevant”
formalisation of causal equivalence for π-calculus in Agda [15]. As long as causality is
respected, an implementation of our system can safely use any technique (e.g. redex trails,
proved transitions, or thread-local memories) to implement rewind and replay.
Example: scheduler with non-compliant task. While dynamic slicing cannot automatically
isolate bugs, it can hide irrelevant detail and yield compact provenance-like explanations
of troublesome parts of configurations. As an example we consider Milner’s scheduler
implementation [12, p. 65]. The scheduler controls a set of n tasks, executed by agents
A1 , . . . , An . Agent Ai sends the message ai (announce) to the scheduler to start its task,
and message bi (break) to end its task. The scheduler ensures that the actions ai occur
cyclically starting with a1 , and that for each i the actions ai and bi alternate, starting with
ai . Although started sequentially, once started the tasks are free to execute in parallel.
Figure 1 shows five transitions of a two-thread scheduler, with the redex selected at each
step highlighted in bold. The parts of the configuration which contribute to the final state
of thread 1 are in black; the grey parts are discarded by our backward-slicing algorithm.
Assume prefixing binds more tightly than either · | · or +. To save space, we omit the
ν-binders defining the various names, and write x.0 simply as x. The names r1 , r2 , p1 and p2
are used to make recursive calls [12, p. 94]: a recursive procedure is implemented as a server
which waits for an invocation request, spawns a new copy of the procedure body, and then
returns to the wait state. Here we omit the server definitions, and simply replace a successful
invocation by the spawned body; thus in the final step of Figure 1, after the synchronisation
on c2 the invocation r1 is replaced by a fresh copy of the initial state of scheduler thread 1.
The final state of Figure 1 has no redexes, and so is stuck. The slice helps highlight the
fact that by the time we come to start the second loop of scheduler 1, the task was terminated
by message b1 from A2 , before any such message could be sent by A1 . We can understand
the slice of the initial configuration (computed by “rewinding”, or backward-slicing) as
sufficient to explain the slice of the stuck configuration by noting that the former is able to
compute the latter by “replay”, or forward-slicing. In other words, writing a sliced part of
the configuration as ◻, and pretending the holes ◻ are sub-computations which get stuck, we
can derive

R. Perera, D. Garg and J. Cheney

18:3

a1 .c1 .(b1 .◻ + ◻) | c1 .a2 .◻ | a1 .◻ | a2 .b1 .p2

−−−→∗

a2 .◻

without getting stuck. The slice on the left may of course choose to take the right-hand
branch of the choice instead. But if we constrain the replay of the sliced program to follow
the causal structure of the original unsliced run – to take the same branches of internal
choices, and have the same synchronisation structure – then it will indeed evolve to the slice
on the right. This illustrates the correctness property for backward slicing, which is that
forward-slicing its result must recompute (at least) the slicing criterion.
For this example, the tasks are entirely atomic and so fixing the outcome of + has the
effect of making the computation completely sequential. Less trivial systems usually have
multiple ways they can evolve, even once the causal structure is fixed. A confluence lemma
typically formalises the observational equivalence of two causally equivalent runs. However,
a key observation made in [15] is that requiring causally equivalent runs to reach exactly the
same state is too restrictive for π-calculus, in particular because of name extrusion. As we
discuss in § 3, two causally unrelated extrusion-rendezvous lead to states which differ in the
relative position of two ν-binders, reflecting the two possible orderings of the rendezvous.
Although technically unobservable to the program, interleaving-sensitive metadata, such
as memory locations in a debugger or transaction ids in a financial application, may be
important for domain-specific reasons. In these situations being able to robustly translate
between the target states of the two executions may be useful.
Summary of contributions. § 2 defines the core forward and backward dynamic slicing
operations for π-calculus transitions and sequences of transitions (traces). We prove that they
are related by a Galois connection, showing that backward and forward slicing, as defined,
are minimal and maximal with respect to each other. § 3 extends this framework to show that
the Galois connections for causally equivalent traces compute the same slices up to lattice
isomorphism. § 4 discusses related work and § 5 offers closing thoughts and prospects for
follow-up work. Appendix A summarises the Agda module structure and required libraries;
the source code can be found at https://github.com/rolyp/concurrent-slicing, release 0.1.

2

Galois connections for slicing π-calculus programs

To summarise informally, our approach is to interpret, functorially, every transition diagram
in the π-calculus into the category of lattices and Galois connections. For example the
interpretation of the transition diagram on the left is the commutative diagram on the right:
↓Q

Q
t

stept

u

P

S
t0

u0
R

stepu

↓P

↓S

stept 0

stepu
↓R

where ↓P means the lattice of slices of P, and stept : ↓P −→ ↓Q is a Galois connection, a
kind of generalised order isomorphism. An order isomorphism between posets A and B is a
pair of monotone functions f : A −→ B and g : B −→ A such that f ◦ g = idB and g ◦ f = idA .
Galois connections require only f ◦ g ≥ idB and g ◦ f ≤ idA where ≤ means the pointwise
order. Galois connections are closed under composition.
The relationship to slicing is that these properties can be unpacked into statements of
sufficiency and minimality: for example f ◦ g ≥ idB means g (backward-slicing) is “sufficient”

CONCUR 2016

Causally consistent dynamic slicing

in that f (forward-slicing) is able to use the result of g to restore the slicing criterion, and
g ◦ f ≤ idA means g is “minimal” in that it computes the smallest slice with that property.
One can dualise these statements to make similar observations about f.
We omit a treatment of structural congruence from our approach, but note that it slots
easily into the framework, generating lattice isomorphisms in a manner similar to the “bound
braid” relation discussed in § 3, Definition 12.
o

18:4

2.1

Lattices of slices

The syntax of names, processes and actions is given in Figure 2. Slices are represented
syntactically, via the ◻ notation introduced informally in § 1. Our formalisation employs de
Bruijn indices [5], an approach with well-known strengths and weaknesses compared to other
approaches to names such as higher-order abstract syntax or nominal calculi.
Name
Payload

x, y ::=
z ::=

0 | 1 | ···
◻

x
Action

a ::=

◻

x
xhzi
x
τ

Process
erased
retained
erased
input
output
bound output
silent

P, Q, R, S ::=

◻

0
x.P
xhzi.P
P +Q
P|Q
νP
!P

erased
inactive
input
output
choice
parallel
restriction
replication

...............................................................................................................................................
Figure 2 Syntax of names, processes and actions

Names. Only names which occur in the “payload” (argument) position of a message may
be erased. The erased name ◻ gives rise to a (trivial) partial order ≤ over payloads, namely
the partial order containing precisely ◻ ≤ z for any z. The set of slices of x is written ↓x
and defined to be {z | z ≤ x}; because names are atomic ↓x is simply the two-element set
{◻, x}. The set ↓x is a finite lattice with meet and join operations u and t, and top and
bottom elements x and ◻ respectively. For any lattice, the meet and join are related to the
underlying partial order by z ≤ z 0 ⇐⇒ z t z 0 = z 0 ⇐⇒ z u z 0 = z. Lattices are closed
under component-wise products, justifying the notation ↓(z, z 0 ) for ↓z × ↓z 0 .
Processes. The ≤ relation and ↓· operation extend to processes, via payloads which may
be ◻, and a special undefined process also written ◻. A slice of P is simply P with some
sub-terms replaced by ◻. The relation ≤ is the least compatible partial order which has
◻ as least element; all process constructors both preserve and reflect ≤, so we assume an
equivalent inductive definition of ≤ when convenient. A process has a closing context Γ
enumerating its free variables; in the untyped de Bruijn setting Γ is just a natural number.
Often it is convenient to conflate Γ with a set of that cardinality.
Actions. An action a labels a transition (Figure 3 below), and is either bound or nonbound. A bound action b is of the form x or x and opens a process with respect to x, taking
it from Γ to Γ + 1. A non-bound action c is of the form xhzi or τ and preserves the free
variables of the process. The ≤ relation and ↓· operation extend to actions via ◻ names, plus
a special undefined action also written ◻.
Renamings. In the lattice setting, a renaming ρ : Γ −→ Γ0 is any function from Γ to
0
Γ ] {◻}; we also allow σ to range over renamings. Renaming application ρ∗ P is extended
with the equation ρ∗ ◻ = ◻. The ≤ relation and ↓· operation apply pointwise.

R. Perera, D. Garg and J. Cheney

18:5

a

c

P −−−→ R
xhzi

x

a

xhzi.P −−−→ P

x.P −−−→ P

P + Q −−−→ R

b

(∗)

(§)

b

x

(†)

τ

P | Q −−−→ ν(R | S)

(x+1)h0i

Q −−−→ S

P −−−→ R

P | Q −−−→ (pop z)∗ R | S

νP −−−→ R

P −−−→ R
τ

P −−−→ R
c

x

push ∗ b

push ∗ c

x

Q −−−→ S

P −−−→ R

c

P | Q −−−→ R | Q

xhzi

x

P −−−→ R
P | Q −−−→ R | push ∗ Q

P −−−→ R

(‡)

νP −−−→ νR

a

P −−−→ R

P | !P −−−→ R

b

a

νP −−−→ ν(swap∗ R)

!P −−−→ R

...............................................................................................................................................
a

Figure 3 Labelled transition relation P −−−→ R (symmetric variants omitted)

Labelled transition semantics. The late-style labelled transition semantics is given in
Figure 3, and is distinguished only by its adaptation to the de Bruijn setting. The primary
reference for a de Bruijn formulation of π-calculus is [9]; the consequences of such an approach
are explored in some depth in [15]. One pleasing consequence of a de Bruijn approach is
that the usual side-conditions associated with transition rules can be operationalised via
renamings. We briefly explain this, along with other uses of renamings in the transition rules,
and refer the interested reader to these earlier works for more details. Definition 1 defines
the renamings used in Figure 3 and Definition 2 the application ρ∗ a of ρ to an action a.
I Definition 1 (push, pop, and swap).
pushΓ
push x

:
=

Γ −→ Γ + 1
x +1

popΓ z
pop z 0
pop z (x + 1)

:
=
=

Γ + 1 −→ Γ
z
x

swapΓ
swap 0
swap 1
swap (x + 2)

:
=
=
=

Γ + 2 −→ Γ + 2
1
0
x +2

I Definition 2 (Action renaming). Define the following lifting of a renaming to actions.
·∗
ρ∗
ρ∗
ρ∗
ρ∗
ρ∗

◻

x
x
τ
xhzi

:
=
=
=
=
=

(Γ −→ Γ0 ) −→ Action Γ −→ Action Γ0
◻

ρx
ρx
τ
ρxhρzi

...............................................................................................................................................
push occurs in the transition rule which propagates a bound action through a parallel
composition P | Q (rule (∗) in Figure 3), and rewires Q so that the name 0 is reserved.
The effect is to ensure that the binder being propagated by P is not free in Q.
push also occurs in the rules which propagate an action through a ν-binder (rules (†)
and (‡)), where it is applied to the action being propagated using the function defined
in Definition 2. This ensures the action does not mention the binder it is propagating
through. The use of · + 1 in the name extrusion rule can be interpreted similarly.
pop z is used in the event of a successful synchronisation (rule (§)), and undoes the effect
of push, substituting the communicated name z for index 0.
swap occurs in the rule which propagates a bound action through a ν-binder (rule (†))
and has no counterpart outside of the de Bruijn setting. As a propagating binder passes
through another binder, their relative position in the syntax is exchanged, and so to
preserve naming R is rewired with a “braid” that swaps 0 and 1.

CONCUR 2016

18:6

Causally consistent dynamic slicing

Although its use in the operational semantics is unique to the de Bruijn setting, swap will
also play an important role when we consider the relationship between slices of causally
equivalent traces (§ 3 below), where it captures how the relative position of binders changes
between different (but causally equivalent) interleavings.

2.2

Galois connections for slicing

We now compositionally assemble a Galois connection for each component of execution,
starting with renamings, and then proceeding to individual transitions and entire traces,
which relates forward and backward slices of the initial and terminal state.
Slicing renamings. The application ρx of a renaming to a name, and the lifting ρ∗ P of
that operation to a process give rise to the Galois connections defined here.
I Definition 3 (Galois connection for ρx). Suppose ρ : Γ −→ Γ0 and x ∈ Γ. Define the
following pair of monotone functions between ↓(ρ, x) and ↓(ρx).
appρ,x
appρ,x
appρ,x

where x 7→ρ ·
(x →
7 ρ z)
(x →
7 ρ z)

↓(ρ, x) −→ ↓(ρx)

:
=
=

(σ , ◻)
(σ , x)
x
y

◻

unappρ,x
unappρ,x

↓(ρx) −→ ↓(ρ, x)
(x 7→ρ z, ρx−1 z)

:
=

z

σx
:
=
=

↓(ρx) −→ ↓ρ
z
◻ (if y 6= x)

ρx−1
ρx−1
ρx−1

◻

z

:
=
=

↓(ρx) −→ ↓x
◻

x

(if z 6= ◻)

...............................................................................................................................................
It is convenient to decompose unappρ,x into two components: x 7→ρ z denotes the least slice
of ρ which maps x to z, and ρx−1 z denotes the least slice of x such that ρx = z.
I Lemma 4. (appρ,x , unappρ,x ) is a Galois connection.
1. appρ,x ◦ unappρ,x ≥ idρx
2. unappρ,x ◦ appρ,x ≤ idρ,x
I Definition 5 (Galois connection for a renaming ρ∗ P).
Suppose ρ : Γ −→ Γ0 and Γ ` P. Define monotone functions between ↓(ρ, P) and ↓(ρ∗ P) by
structural recursion on ↓P, using the following equations. Here ◻ρ denotes the least slice of
ρ, namely the renaming which maps every x ∈ Γ to ◻.
renρ,P
renρ,P
renρ,0
renρ,x.P
renρ,xhzi.P
renρ,P+Q
renρ,P|Q
renρ,νP
renρ,!P
unrenρ,P
unrenρ,P
unrenρ,0
unrenρ,x.P
unrenρ,xhzi.P
unrenρ,P+Q
unrenρ,P|Q
unrenρ,νP
unrenρ,!P

(σ , ◻)
(σ , 0)
(σ , x.R)
(σ , xhz 0 i.R)
(σ , R + S)
(σ , R | S)
(σ , νR)
(σ , !R)

◻

0
x.R
xhz 0 i.R
(R + S)
(R | S)
νR
!R

↓(ρ, P) −→ ↓(ρ∗ P)

:
=
=
=
=
=
=
=
=

0
x.renρ+1,P (σ , R)
xhz 00 i.renρ,P (σ , R) where z 00 = appρ,y (σ , z 0 )
renρ,P (σ , R) + renρ,Q (σ , S)
renρ,P (σ , R) | renρ,Q (σ , S)
ν(renρ+1,P (σ + 1, R)
!(renρ,P (σ , R))

:
=
=
=
=
=
=
=
=

↓(ρ∗ P) −→ ↓(ρ, P)
( ◻ρ , ◻)
(◻ρ , 0)
(ρ0 , x.P 0 ) where unrenρ+1,P R = (ρ0 + 1, P 0 )
(ρ0 t (z 7→ρ z 0 ), xhz 00 i.P 0 ) where unrenρ,P R = (ρ0 , P 0 ) and z 00 = ρz−1 z 0
(ρ1 t ρ2 , P 0 + Q 0 ) where unrenρ,P R = (ρ1 , P 0 ) and unrenρ,Q S = (ρ2 , Q 0 )
(ρ1 t ρ2 , P 0 | Q 0 ) where unrenρ,P R = (ρ1 , P 0 ) and unrenρ,Q S = (ρ2 , Q 0 )
(ρ0 , νP 0 ) where unrenρ+1,P R = (ρ0 + 1, P 0 )
(ρ0 , !P 0 ) where unrenρ,P R = (ρ0 , P 0 )

◻

...............................................................................................................................................

R. Perera, D. Garg and J. Cheney

18:7

a0

x

◻

◻P

a
−−−
+ ◻P 0

b0

RP | SQ −−−+ RP0 0 | SQ

RP | SQ −−−+ RP0 0 | push∗ SQ

b0b

xhz 0 i

◻

a

◻τ

RP | SQ −−−+ (pop

∗
zz0 ) RP0 0

|

x

RP −−−+ RP0 0

SQ −−−+ SQ0 0
τ

push∗ c 0

RP0 0

(x+1)h0i

RP −−−+ RP0 0
x

SQ0 0

|

νRP −−−+ RP0 0
a0

a

x
+ RP0 0
RP −−−

x
SQ −−−
+ SQ0 0

◻

τ
+ ν(RP0 0 | SQ0 0 )
RP | SQ −−−

RP | SQ −−−+ ν(RP0 0 | SQ0 0 )

◻

x
νRP −−−
+ RP0 0

∗

◻

∗

RP | SQ −−−+ (pop ◻z )

x

a

RP −(x+1)h0i
−−+ RP0 0

τ

RP | SQ −−−+ (pop zz0 ) RP0 0 | SQ0 0

◻τ

SQ0 0

SQ −−−z+ SQ0 0

−+ SQ0 0
SQ −−xhzi

x
RP −−−
+ RP0 0

SQ −−−z+ SQ0 0

xhz 0 i

x

b
RP −−−
+ RP0 0

x
RP −−−
+ RP0 0

a
RP + SQ −−−
+ RP0 0

RP −−−+ RP0 0

c
RP −−−
+ RP0 0

cc0

a0

xhzz0 i.RP −−−+ RP

x.RP −−−+ RP

c0

a
RP −−−
+ RP0 0

xhzz0 i

push∗ b0

a0

RP −−−+c RP0 0

RP −−−+b RP0 0

a
RP | !RP −−−
+ RP0 0

c
νRP −−−
+ νRP0 0

b
νRP −−−
+ ν(swap∗ RP0 0 )

a
!RP −−−
+ RP0 0

c0

b0

a0

...............................................................................................................................................
a0

a
Figure 4 Forward slicing judgement RP −−−
+ RP0 0

I Lemma 6. (renρ,P , unrenρ,P ) is a Galois connection.
1. renρ,P ◦ unrenρ,P ≥ idρ∗ P
2. unrenρ,P ◦ renρ,P ≤ idρ,P
Proof. In each case by induction on P, using Lemma 4 and the invertibility of · + 1.

J

Slicing transitions. Transitions also lift to the lattice setting, in the form of Galois
a
connections defined by structural recursion over the proof that t : P −−−→ P 0 . Figures 4
and 5 define the forward and backward slicing judgements. We assume a determinising
convention where a rule applies
only if no earlier rule applies.
a0a
The judgement RP −−−
+ RP0 0 asserts that there is a “replay” transition from R0 ≤ P
aa
to (a0 , R 0 ) ≤ (a, P), with R the input and (a0 , R 0 ) the output. The judgement RP0 )−−
− RP 0
asserts that there is a “rewind” transition from (a0 , R) ≤ (a, P 0 ) to R 0 ≤ P, with (a0 , R) the
input and R 0 the output. When writing RP where R ≤ P we exploit the preservation and
reflection of ≤ by all constructors, for example writing ν(RP | SQ ) for ν(R | S)ν(P|Q) .
For backward slicing, we permit the renaming application operator ∗ to be used in
a pattern-matching form, indicating a use of the lower adjoint unren: given a renaming
application ρ∗ P, the pattern σ ∗ P 0 matches any slice R of ρ∗ P such that unrenρ,P (R) = (σ , P 0 ).
a

I Definition 7 (Galois connection for a transition). Suppose t : P −−−→ P 0 . Define the
following pair of monotone functions between ↓P to ↓(a, P 0 ).
stept
stept

R

:
=

↓P −→ ↓(a, P 0 )
a0a
(a0 , R 0 ) where RP −−−
+ RP0 0

unstept
unstept

0

(R, a )

:
=

↓(a, P 0 ) −→ ↓P
a0a
R 0 where RP0 )−−
− RP 0

...............................................................................................................................................
We omit the proofs that these equations indeed define total, deterministic, monotone relations.
I Theorem 8 ((stept , unstept ) is a Galois connection).
1. stept ◦ unstept ≥ ida,P 0
2. unstept ◦ stept ≤ idP
a0

Proof. By induction on t : P −−−→ P 0 , using Lemma 6 for the cases involving renaming.

J

CONCUR 2016

18:8

Causally consistent dynamic slicing

xhz 0 i

a

◻

a
)−−
− ◻P 0

◻P

a0

◻

z
xhzz0 i.RP )−−
− RP

x
x.RP )−−
− RP

xh◻z i.RP )−xhzi
−− RP

c0

c0

a
RP0 )−−
− RP 0

c
RP0 )−−
− RP 0

c
RP0 )−−
− ◻P 0

RP0 + ◻Q )−−− RP 0

RP0 | SQ )−−− RP 0 | SQ

c
RP0 | ◻Q )−−
− ◻P 0 |Q

a0a

cc0

b0

RP0 )−−− RP 0

RP0 )−−− ◻P 0

b
RP0 | SQ )−−
− RP 0 | ρpush ∗ SQ

RP0 | ◻Q )−−− ◻P 0 |push∗ Q

◻

x
RP0 )−−
− RP 0

xhzi

SQ0 )−−− SQ 0

RP0 | SQ0 )−−− ρpop z ∗ RP 0 | SQ 0

◻

xh◻ i

x

◻

x
− ◻Q 0
SQ )−−

RP | SQ )−−− ν ◻P 0 |Q 0
x

RP0 )−−− RP 0

SQ )−−− ◻Q 0

c0

τ

◻

c
− νRP 0
νRP0 )−−

RP | SQ )−−− ◻ν(P 0 |Q 0 )

RP0 )−−− ◻P 0

RP0 )−−− RP 0

push∗ b0

RP0 )−−− ◻P 0

νRP0 )−−− ◻νP 0

νRP0 )−−− ν(ρswap ∗ RP 0 )

νRP0 )−−− ◻ν(swap∗ P 0 )

cc0

push∗ c 0

x

RP )−−− ◻P 0

τ
RP | SQ )−−
− ν ◻P 0 |Q 0

push∗ c 0

SQ )−−− ◻Q 0
τ

◻

◻

x

RP )−−− ◻P 0

τ
RP0 | SQ0 )−−
− ν(RP 0 | SQ 0 )
x
RP )−−
− ◻P 0

x

SQ0 )−−− SQ 0

RP0 | SQ0 )−−− ν(RP 0 | SQ 0 )
x

x
SQ0 )−−
− SQ 0

ρ0 = ◻

τ

νRP0 )−−− RP 0
◻

x
RP0 )−−
− RP 0

x

RP0 )−−− RP 0

ax

RP | SQ )−−− ◻(pop z)∗ P 0 |Q 0
◻

RP0 | SQ0 )−−− ρpop z ∗ RP 0 | SQ 0
(x+1)h0i

τ

ρ0 = z 0

◻

SQ0 )−xhzi
−− SQ 0

◻τ

RP0 )−−− RP 0

SQ )−−z− ◻Q 0

RP )−−− ◻P 0

RP0 | SQ0 )−−− ρpop z ∗ RP 0 | SQ 0

x
RP0 )−−
− RP 0

ρ0 = z

z
SQ0 )−−
− SQ 0

τ

b

◻τ

xhz 0 i

x

b

b
RP0 )−−
− RP 0

b0

c0

push∗ b

b0b

a0

2
a
)−−
− RP 0
RP0 | R!P

b

a0

a
(!R 0 t R 2 )!P )−−
− RP 0

...............................................................................................................................................
a0

a
− RP 0
Figure 5 Backward slicing judgement RP0 )−−

Slicing traces. Finally we extend slicing to entire runs of a π-calculus program. A
sequence of transitions t̃ is called a trace; the empty trace at P is written εP , and the
a
ã
a ã
composition of a transition t : P −−−→ R and trace t̃ : R −−−→ S is written t · t̃ : P −−·−→ S
where actions are composable whenever their source and target contexts match.
ã

I Definition 9 (Galois connection for a trace). Suppose t̃ : P −−−→ P 0 . Define the following
pair of monotone functions between ↓P and ↓P 0 , using variants of stept and unstept which
discard the action slice (going forward) and which use ◻ as the action slice (going backward).
...............................................................................................................................................
↓P −→ ↓P 0
id↓P

fwdt̃
fwdεP
fwdt ·t̃ ◻
fwdt ·t̃ R

:
=
=
=

fwdt̃ (step0t R)

step0t
step0t R

:
=

↓P −→ ↓P0
R 0 where stept R = (a0 , R 0 )

◻

(R 6= ◻)

bwdt̃
bwdεP 0
bwdt ·t̃ ◻
bwdt ·t̃ R

:
=
=
=

unstep0t
unstep0t R 0

:
=

↓P 0 −→ ↓P
id↓P 0

◻

unstep0t (bwdt̃ R)

(R 6= ◻)

↓P 0 −→ ↓P
unstept (◻, R 0 )

...............................................................................................................................................
At the empty trace εP the Galois connection is simply the identity on ↓P. Otherwise, we
recurse into the structure of the trace t · t̃, composing the Galois connection for the single
transition t with the Galois connection for the tail of the computation t̃.
I Theorem 10 ((fwdt̃ , bwdt̃ ) is a Galois connection).
1. fwdt̃ ◦ bwdt̃ ≥ idP 0

R. Perera, D. Garg and J. Cheney

18:9

2. bwdt̃ ◦ fwdt̃ ≤ idP
Note that the trace used to define forward and backward slicing for a computation is not an
auxiliary data structure recording the computation, such as a redex trail or memory, but
ã
simply the proof term witnessing P −−−→ P 0 .

3

Slicing and causal equivalence

In this section, we show that when dynamic slicing a π-calculus program, slicing with respect
to any causally equivalent execution yields essentially the same slice. “Essentially the same”
here means modulo lattice isomorphism. In other words slicing discards precisely the same
information regardless of which interleaving is chosen to do the slicing.
Proof-relevant causal equivalence. Causally equivalent computations are generated by
transitions which share a start state, but which are independent. Following Lévy [11], we
call such transitions concurrent, written t ^ t 0 . We illustrate this idea, and the non-trivial
relationship that it induces between terminal states, by way of example. For the full definition
of concurrency for π-calculus, we refer the interested reader to [15] or to the Agda definition1 .
For the sake of familiarity the example uses regular names instead of de Bruijn indices.
def
Example. Consider the process P0 = (νyz) (xhyi.P) | xhzi.Q for some unspecified
processes P and Q. This process can take two transitions, which we will call t and t 0 .
x(y)
Transition t : P0 −−−→ P1 extrudes y on the channel x:
def

x(y)

P0 −−−→ (νz) P | xhzi.Q = P1
x(z)

whereas transition t 0 : P0 −−−→ P10 extrudes z, also on the channel x:
def

x(z)

P0 −−−→ (νy) (xhyi.P) | Q = P10

In both cases the output actions are bound, representing the extruding binder. Moreover, t
and t 0 are concurrent, written t ^ t 0 , meaning they can be executed in either order. Having
taken t, one can mutatis mutandis take t 0 , and vice versa. Concurrency is an irreflexive and
symmetric relation defined over transitions which are coinitial (have the same source state).
The qualification is needed because t 0 will need to be adjusted to operate on the target
state of t, if t is the transition which happens first. If t 0 happens first then t will need to be
adjusted to operate on the target state of t 0 . The adjusted version of t 0 is called the residual
of t 0 after t, and is written t 0 /t. In this case t 0 /t can still extrude z:
def

x(z)

P1 = (νz) P | xhzi.Q −−−→ P | Q = P00

whereas the residual t/t 0 can still extrude y:
x(y)

P10 = (νy) (xhyi.P) | Q −−−→ P | Q = P00

The independence of t and t 0 is confirmed by the fact that t
(share a target state), as shown on the left below.

↓P1

P1
t 0 /t

t

P00

P0
t0

t/t 0
P10

1

· t 0 /t and t 0 · t/t 0 are cofinal
stept 0 /t

stept

↓P00

↓P0
stept 0

↓P10

stept/t 0

https://github.com/rolyp/proof-relevant-pi/blob/master/Transition/Concur.agda

CONCUR 2016

18:10

Causally consistent dynamic slicing
def

def

We say that the traces t̃ = t · t 0 /t and ũ = t 0 · t/t 0 are causally equivalent, written t̃ ' ũ. The
commutativity of the right-hand square (Theorem 16 below) means the two interleavings are
also equivalent for slicing purposes. Here stept denotes the Galois connection (stept , unstept ).
However [15], which formalised causal equivalence for π-calculus, showed that causally
equivalence traces do not always reach exactly the same state, but only the same state up
to some permutation of the binders in the resulting processes. This will become clear if
def
we consider another process Q0 = (x(y0 ).R) | x(z 0 ).S able to synchronise with both of the
extrusions raised by P0 and consider the two different ways that P0 | Q0 0 can evolve.
def
x(y )
First note that Q0 can also take two independent transitions: u : Q00 −−−→ R | x(z 0 ).S = Q1
def
x(z
)
inputs on x and binds the received name to y0 ; and u0 : Q0 −−−→ (x(y0 ).R) | S = Q10
also inputs on x and binds the received name to z 0 . (Assume z is not free in the lefthand side of Q0 and0 that y is not free in the right-hand side.)
The respective residuals
def
x(z )
x(y0 )
0
0
0
0
Q1 = R | x(z ).S −−−→ R | S = Q0 and Q1 = (x(y ).R) | S −−−→ R | S = Q00 again converge
on the same state Q00 , leading to a diamond for Q0 similar to the one for P0 above.
The subtlety arises when we put P0 and Q0 into parallel composition, since now we have
two concurrent synchronisation possibilities. For clarity we give the derivations, which we
call s and s0 :
x(y)

t : P0 −−−→ P1

x(y0 )

x(z)

t 0 : P0 −−−→ P10

u : Q0 −−−→ Q1

τ

x(z 0 )

u0 : Q0 −−−→ Q10

τ

s0 : P0 | Q0 −−−→ (νz) P10 | Q10 {z/z 0 }

s : P0 | Q0 −−−→ (νy) P1 | Q1 {y/y0 }

The labelled transition system is closed under renamings; thus the residual u0 /u has an image
in the renaming ·{y/y0 }, and u/u0 has an image in the renaming ·{z/z 0 }, allowing us to derive
composite residual s0 /s:
x(z 0 )

u0 /u : Q1 −−−→ Q00
x(z 0 )

x(z)

t 0 /t : P1 −−−→ P00

(u0 /u){y/y0 } : Q1 {y/y0 } −−−→ Q00 {y/y0 }
τ

s0 /s : (νy) P1 | Q1 {y/y0 } −−−→ (νyz) P00 | Q00 {y/y0 }{z/z 0 }

By similar reasoning we can derive s/s0 :
τ

s/s0 : (νz) P10 | Q10 {y/y0 } −−−→ (νzy) P00 | Q00 {z/z 0 }{y/y0 }

By side-conditions on the transition rules the renamings ·{y/y0 } and ·{z/z 0 } commute and
def
so Q00 {y/y0 }{z/z 0 } = Q02 = Q00 {z/z 0 }{y/y0 }. However, the positions of binders y and z are
transposed in the terminal states of s0 /s and s/s0 . Instead of the usual diamond shape, we
have the pentagon on the left below, where φ is a braid representing the transposition of
the binders. Lifted to slices, φ becomes the unique isomorphism braidφ relating slices of the
terminal states, as shown in the commutative diagram on the right:
(νz) P1 | Q1 {y/y0 }

s0 /s

(νyz) P00 | Q000

steps0 /s

↓((νyz) P00 | Q000 )

steps

s

↓(P0 | Q0 )

φ

P0 | Q0
s0
(νy)

↓((νz) P1 | Q1 {y/y0 })

braidφ

steps0
P10

|

Q10 {z/z 0 }

s/s0

(νzy)

P00

|

Q000

↓((νy) P10 | Q10 {z/z 0 })

steps/s0

↓((νzy) P00 | Q000 )

In the de Bruijn setting, a braid like φ does not relate two processes of the form (νyz) R
and (νyz) R but rather two processes of the form ννR and νν(swap∗ R): the transposition of
the (nameless) binders is represented by the transposition of the roles of indices 0 and 1 in
the body of the innermost binder.

R

P|·

R |Q

Q
P|Q

P
P +Q

S

R

P

ν·

P|S

P +·

R +Q

νP

R

Q
P +Q
!·

νR

P
!P

o o

·+Q

o

R

S
P +S

o o

P = swap∗ P 0

o o

R). Inductively define the symmetric relation P

o o

P
P|Q

ννP 0

18:11

o o

·|Q

ννP

o o

νν-swapP

o

I Definition 11 (Bound braid P
using the rules below.

o

R. Perera, D. Garg and J. Cheney

R
!R

...............................................................................................................................................
o

Following [15], we adopt a compact term-like notation for proofs, using the rule names
which occur to the left of each rule in Definition 11. For the extrusion example above, φ (in
de Bruijn indices notation) would be a leaf case of the form νν-swap·|· .
o

I Definition 12 (Lattice isomorphism for bound braid). Suppose φ : Q
Q 0 . Define the
0
following pair of monotone functions between ↓Q and ↓Q by structural recursion on φ.
braidφ
braidνν-swapP
braidφ+S
braidR+ψ
braidφ|S
braidR|ψ
braidνφ
braid!φ

(ννR)
(R + S)
(R + S)
(R | S)
(R | S)
(νR)
(!R)

↓Q −→ ↓Q 0
νν(renswap,P (R))
braidφ R + S
R + braidψ S
braidφ R | S
R | braidψ S
ν(braidφ R)
!(braidφ R)

:
=
=
=
=
=
=
=

unbraidφ
unbraidνν-swapP
unbraidφ+S
unbraidR+ψ
unbraidφ|S
unbraidR|ψ
unbraidνφ
unbraid!φ

(ννR)
(R + S)
(R + S)
(R | S)
(R | S)
(νR)
(!R)

:
=
=
=
=
=
=
=

↓Q 0 −→ ↓Q
νν(renswap,P (R))
unbraidφ R + S
R + unbraidψ S
unbraidφ R | S
R | unbraidψ S
ν(unbraidφ R)
!(unbraidφ R)

...............................................................................................................................................
I Lemma 13.
1. braidφ ◦ unbraidφ = id↓Q 0
2. unbraidφ ◦ braidφ = id↓Q
Proof. Induction on φ. In the base case use the idempotence of swap lifted to lattices.

J

o

↓Q −→ ↓Q 0
id↓Q
renswap,Q
braidφ

n

o

unmapγt,t 0
unmapQ=Q 0
unmapQ Q 0
unmapφ:Q Q 0
n

:
=
=
=

mapγt,t 0
mapQ=Q 0
mapQ Q 0
mapφ:Q Q 0

o

n

I Definition 14 (Lattice isomorphism for cofinality map). Suppose t ^ t 0 with tgt(t 0 /t) = Q
and tgt(t/t 0 ) = Q 0 . By Theorem 1 of [15], there exists a unique γt,t 0 witnessing Q = Q 0 ,
Q Q 0 or Q Q 0 . Define the following pair of monotone functions between ↓Q and ↓Q 0 .
:
=
=
=

↓Q 0 −→ ↓Q
id↓Q
unrenswap,Q
unbraidφ

...............................................................................................................................................
I Lemma 15.
1. mapγt,t0 ◦ unmapγt,t0 = id↓Q 0
2. unmapγt,t0 ◦ mapγt,t0 = id↓Q
I Theorem 16. Suppose t ^ t 0 as on the left. Then the pentagon on the right commutes.
R

t 0 /t

Q

↓R

stept 0 /t

↓Q

stept

t
γt,t 0

P
t0

mapγt,t0

↓P
stept 0

R

0

t/t 0

Q0

↓R 0

stept/t 0

↓Q 0

CONCUR 2016

18:12

Causally consistent dynamic slicing

Lattice isomorphism for arbitrary causal equivalence. Concurrent transitions t ^ t 0
induce an “atom” of causal equivalence, t · t 0 /t ' t 0 · t/t 0 . The full relation is generated by
closing under the trace constructors (for horizontal composition) and transitivity (for vertical
composition). In [15] this yields a composite form of cofinality map γα where α : t̃ ' ũ is an
arbitrary causal equivalence. We omit further discussion for reasons of space, but note that
γα is built by composing and translating (by contexts) atomic cofinality maps, and so gives
rise, by composition of isomorphisms, to a lattice isomorphism between ↓tgt(t̃) and ↓tgt(ũ).

4

Related work

Reversible process calculi. Reversible process calculi have recently been used for speculative
execution, debugging, transactions, and distributed protocols that require backtracking. A
key challenge is to permit backwards execution to leverage concurrency whilst ensuring causal
consistency. In contrast to our work, reversible calculi focus on mechanisms for reversibility,
such as the thread-local memories used by Danos and Krivine’s reversible CCS [4], Lanese et
al’s ρπ [10], and Cristescu et al’s reversible π-calculus [3]. We intentionally remain agnostic
about implementation strategy, whilst providing a formal guarantee that causally consistent
rewind and replay are a suitable foundation for any implementation.
Concurrent program slicing. An early example of concurrent dynamic slicing is Duesterwald et al, who consider a language with synchronous message-passing [7]. They give a
notion of correctness with respect to a slicing criterion, but find that computing least slices is
undecidable, in contrast to our slices which are extremal by construction. Following Cheng [2],
most subsequent work has recast dynamic slicing as a dependency-graph reachability problem;
our approach is to slice with respect to a particular interleaving, but show how to derive the
slice corresponding to any execution with the same dependency structure.
Goswami and Mall consider shared-memory concurrency [8], and Mohapatra et al tackle
slicing for concurrent Java [13], but both present only algorithms, with no formal guarantees.
Tallam et al develop an approach based on dependency graphs, but again offer only algorithms
and empirical results [17]. Moreover most prior work restricts the slicing criteria to the
(entire) values of particular variables, rather than arbitrary parts of configurations.
Provenance and slicing. Our interest in slicing arises in part due to connections with
provenance, and recent applications of provenance to security [1]. Others have also considered
provenance models in concurrency calculi, including Souliah et al [16] and Dezani-Ciancaglini
et al [6]. Further study is needed to relate our approach to provenance and security.

5

Conclusion

The main contribution of this paper is to extend our previous approach to slicing based on
Galois connections to π-calculus, and show that the resulting notion of slice is invariant
under causal equivalence. For this latter step, we build on a prior formalisation of causal
equivalence for π-calculus [15]. Although de Bruijn indices significantly complicate the
resulting definitions, the formalism is readily implemented in Agda. This paper provides
a foundation for future development of rigorous provenance tracing or dynamic slicing
techniques for practical concurrent programs, which we plan to investigate in future work.
Acknowledgements. Perera and Cheney were supported by the Air Force Office of Scientific
Research, Air Force Material Command, USAF, under grant number FA8655-13-1-3006. The
U.S. Government and University of Edinburgh are authorized to reproduce and distribute

R. Perera, D. Garg and J. Cheney

18:13

reprints for their purposes notwithstanding any copyright notation thereon. Perera was
also supported by UK EPSRC project EP/K034413/1. Umut Acar helped with problem
formulation and an earlier approach. Vít Šefl provided valuable Agda technical support. Our
anonymous reviewers provided useful comments.
References
1
2
3
4
5

6
7

8
9
10

11

12
13

14

15
16
17

18

Umut A. Acar, Amal Ahmed, James Cheney, and Roly Perera. A core calculus for provenance. Journal of Computer Security, 21:919–969, 2013. Full version of a POST 2012 paper.
Jingde Cheng. Slicing concurrent programs: A graph-theoretical approach. In Automated
and Algorithmic Debugging, number 749 in LNCS, pages 223–240. Springer-Verlag, 1993.
Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the
reversible pi-calculus. pages 388–397, June 2013.
Vincent Danos and Jean Krivine. Reversible communicating systems. In Concurrency
Theory, 15th International Conference, CONCUR ’04, pages 292–307. Springer, 2004.
N.G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic
formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381–392, 1972.
M. Dezani-Ciancaglini, R. Horne, and V. Sassone. Tracing where and who provenance in
linked data: A calculus. Theoretical Computer Science, 464:113–129, 2012.
Evelyn Duesterwald, Rajiv Gupta, and Mary Lou Soffa. Distributed slicing and partial
re-execution for distributed programs. In Proceedings of the 5th International Workshop
on Languages and Compilers for Parallel Computing, pages 497–511. Springer, 1993.
D. Goswami and R. Mall. Dynamic slicing of concurrent programs. In High Performance
Computing – HiPC 2000, volume 1970, pages 15–26. Springer, 2000.
Daniel Hirschkoff. Handling substitutions explicitly in the pi-calculus. In 2nd International
Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 1999.
Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversing higher-order π.
In Concurrency Theory, 21st International Conference, CONCUR ’10, pages 478–493.
Springer, 2010.
Jean-Jacques Lévy. Optimal reductions in the lambda-calculus. In J. P. Seldin and J. R.
Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and
Formalism, pages 159–191. Academic Press, New York, NY, USA, 1980.
Robin Milner. Communicating and mobile systems: the π calculus. Cambridge University
Press, Cambridge, UK, 1999.
D.P. Mohapatra, Rajib Mall, and Rajeev Kumar. An efficient technique for dynamic slicing
of concurrent Java programs. In Applied Computing, volume 3285, pages 255–262. Springer,
2004.
Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. Functional programs
that explain their work. In 17th ACM SIGPLAN International Conference on Functional
Programming, ICFP ’12, pages 365–376. ACM, 2012.
Roly Perera and James Cheney. Proof-relevant pi-calculus, 2016. Submitted to Mathematical Structures in Computer Science. http://arxiv.org/abs/1604.04575.
Issam Souilah, Adrian Francalanza, and Vladimiro Sassone. A formal model of provenance
in distributed systems. In TAPP 2009, Berkeley, CA, USA, 2009. USENIX Association.
Sriraman Tallam, Chen Tian, and Rajiv Gupta. Dynamic slicing of multithreaded programs
for race detection. In 24th IEEE International Conference on Software Maintenance (ICSM
2008), pages 97–106. IEEE, 2008.
Mark Weiser. Program slicing. In Proceedings of the 5th International Conference on
Software Engineering, ICSE ’81, pages 439–449, Piscataway, NJ, USA, 1981. IEEE Press.

CONCUR 2016

18:14

Causally consistent dynamic slicing

A

Agda module structure

Figure 6 summarises the module structure of the repository concurrent-slicing, which
contains the Agda formalisation. The module structure of the auxiliary repositories is
described in [15]. All repositories can be found at the URL https://github.com/rolyp.
Auxiliary repositories
Extensions to Agda library
Concurrent transitions, residuals and causal equivalence

agda-stdlib-ext 0.0.3
proof-relevant-pi 0.3

Core modules
Action slices a0 ∈ ↓a
Action residual, lifted to slices
Action renaming, lifing to slices
Bound braids, lifted to slices via braidφ and unbraidφ
Include everything; compile to build project
Common imports from standard library
Milner’s scheduler example
Utility functions for examples
Lattice typeclass
Component-wise product of lattices
Name slices y ∈ ↓x
Process slices P 0 ∈ ↓P
Process renaming, lifted to slices via renρ,P and unrenρ,P
Renaming slices σ ∈ ↓ρ and application to slices (appρ,x and unappρ,x )
Additional properties relating to renaming slices
Slicing functions stept and unstepgt
Renaming of transitions, lifted to lattices

Action.Lattice
Action.Concur.Lattice
Action.Ren.Lattice
Braiding.Proc.Lattice
ConcurrentSlicing
ConcurrentSlicingCommon
Example
Example.Helper
Lattice
Lattice.Product
Name.Lattice
Proc.Lattice
Proc.Ren.Lattice
Ren.Lattice
Ren.Lattice.Properties
Transition.Lattice
Transition.Ren.Lattice
Transition.Concur.Cofinal.Lattice
Transition.Seq.Lattice

Braidings γt,t 0 lifted to slices
Slicing functions fwdt̃ and bwdt̃

Common sub-modules
.GaloisConnection

Galois connection between lattices defined in parent module

...............................................................................................................................................
Figure 6

concurrent-slicing

module overview, release

0.1

