Implementing
EscapeContinuations inC
Jean-Michel
Hufflen
PlanImplementing Escape Continuations in C

Motivation
Continuation
semantics
ExamplesJean-Michel Hufflen

BridgeScheme/C

University of Franche-Comté, CNRS,FEMTO-ST institute, F-25000 Besançon, France

Future work

14 December 2023

1/1/16

Implementing
EscapeContinuations inC
Jean-Michel
Hufflen

Motivation

PlanMotivation

Continuation semantics

Continuation
semantics
ExamplesExamplesBridgeScheme/C
Future work

Bridge Scheme/C
Future work

2/2/16

Implementing
EscapeContinuations inC

Functions setjmp and longjmp

Jean-Michel
Hufflen

Included into the C language:

PlanMotivation#include <setjmp.h>

Continuation
semantics

int setjmp(jmp_buf env) ;void longjmp(jmp_buf env, int val) ;ExamplesBridgeScheme/C
Future work

3/3/16

Implementing
EscapeContinuations inC

Functions setjmp and longjmp

Jean-Michel
Hufflen

Included into the C language:

PlanMotivation#include <setjmp.h>

Continuation
semantics

int setjmp(jmp_buf env) ;void longjmp(jmp_buf env, int val) ;Examplessetjmp(env) memoizes the current environment into theenv variable and returns 0.

Future work

BridgeScheme/C

4/3/16

Implementing
EscapeContinuations inC

Functions setjmp and longjmp

Jean-Michel
Hufflen

Included into the C language:

PlanMotivation#include <setjmp.h>

Continuation
semantics

int setjmp(jmp_buf env) ;void longjmp(jmp_buf env, int val) ;Examplessetjmp(env) memoizes the current environment into theenv variable and returns 0.
longjmp(env,val) starts over from the return point where
env was saved, but the returned value at this point is nowval.

Future work

BridgeScheme/C

5/3/16

Implementing
EscapeContinuations inC

Using setjmp/longjmp
If you write something like:

Jean-Michel
Hufflenif (setjmp(env)) |{z}. . . ; else |{z}... ;ËPlanÊ

Motivationthat allows you to start a computation at Ê; if you want toescape it, use:

Continuation
semantics
ExamplesBridgeScheme/C

longjmp(env,1)

Future workand the computation will terminate by running Ë, getting ridof Ê.

6/4/16

Implementing
EscapeContinuations inC

Using setjmp/longjmp
If you write something like:

Jean-Michel
Hufflenif (setjmp(env)) |{z}. . . ; else |{z}... ;ËPlanÊ

Motivationthat allows you to start a computation at Ê; if you want toescape it, use:

Continuation
semantics
ExamplesBridgeScheme/C

longjmp(env,1)

Future workand the computation will terminate by running Ë, getting ridof Ê.
A kind of goto, but to a place already reached,

7/4/16

Implementing
EscapeContinuations inC

Using setjmp/longjmp
If you write something like:

Jean-Michel
Hufflenif (setjmp(env)) |{z}. . . ; else |{z}... ;ËPlanÊ

Motivationthat allows you to start a computation at Ê; if you want toescape it, use:

Continuation
semantics
ExamplesBridgeScheme/Clongjmp(env,1)

Future workand the computation will terminate by running Ë, getting ridof Ê.
A kind of goto, but to a place already reached, or a kind ofbacktrack.

8/4/16

Implementing
EscapeContinuations inC

Using setjmp/longjmp
If you write something like:

Jean-Michel
Hufflenif (setjmp(env)) |{z}. . . ; else |{z}... ;ËPlanÊ

Motivationthat allows you to start a computation at Ê; if you want toescape it, use:

Continuation
semantics
ExamplesBridgeScheme/C

longjmp(env,1)

Future workand the computation will terminate by running Ë, getting ridof Ê.
A kind of goto, but to a place already reached, or a kind of
backtrack.
These functions have been used to implement a roughmechanism of exceptions but, in reality, they are closed tocontinuations.
9/4/16

Implementing
EscapeContinuations inC

Continuations in Scheme(F1 (call/cc G1 )) ≡ (F1 (G1Jean-Michel
Hufflen←−F61 ))

PlanIf F1 is invoked within G1 ’s body, it is applied and yields a
direct result, without returning to a caller.

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

10/5/16

Implementing
EscapeContinuations inC

Continuations in Scheme(F1 (call/cc G1 )) ≡ (F1 (G1Jean-MichelHufflen←−F61 ))Plan

If F1 is invoked within G1 ’s body, it is applied and yields a
direct result, without returning to a caller. ‘(F1 ...)’ is for‘normal’ run.

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

11/5/16

Implementing
EscapeContinuations inC

Continuations in Scheme(F1 (call/cc G1 )) ≡ (F1 (G1Jean-Michel
Hufflen←−F61 ))Plan

If F1 is invoked within G1 ’s body, it is applied and yields a
direct result, without returning to a caller. ‘(F1 ...)’ is for‘normal’ run.
Examples:(+ 1 (call/cc (lambda (f1) (* 2 (f1 2023))))) =⇒2024(+ 1 (call/cc (lambda (f1) (* 2 2023)))) =⇒ 4047

12/5/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

Continuations in Scheme(F1 (call/cc G1 )) ≡ (F1 (G1Jean-MichelHufflen←−F61 ))Plan

If F1 is invoked within G1 ’s body, it is applied and yields a
direct result, without returning to a caller. ‘(F1 ...)’ is for‘normal’ run.
Examples:(+ 1 (call/cc (lambda (f1) (* 2 (f1 2023))))) =⇒2024(+ 1 (call/cc (lambda (f1) (* 2 2023)))) =⇒ 4047
Continuations captured by means of the call/cc function
may be saved and applied overwhelmingly, but we are notinterested in this feature.

13/5/16

MotivationContinuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

Continuations in Scheme(F1 (call/cc G1 )) ≡ (F1 (G1Jean-Michel
Hufflen←−F61 ))Plan

If F1 is invoked within G1 ’s body, it is applied and yields a
direct result, without returning to a caller. ‘(F1 ...)’ is for‘normal’ run.
Examples:(+ 1 (call/cc (lambda (f1) (* 2 (f1 2023))))) =⇒2024(+ 1 (call/cc (lambda (f1) (* 2 2023)))) =⇒ 4047
Continuations captured by means of the call/cc functionmay be saved and applied overwhelmingly, but we are notinterested in this feature.
call/ec ⇐= escape continuations, dynamic extent only.
14/5/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

Programming languages with continuations

Jean-Michel
Hufflen
Plan
Motivation

call/cc present in some languages, e.g., Ruby.

Continuation
semantics
ExamplesBridgeScheme/C
Future work

15/6/16

Implementing
EscapeContinuations inC

Programming languages with continuations

Jean-Michel
HufflenPlancall/cc present in some languages, e.g., Ruby.
Standard ML of New Jersey provides typed continuations,and escape continuations as typed control continuations(being ’a control_cont type).

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

16/6/16

Implementing
EscapeContinuations inC

Programming languages with continuations

Jean-Michel
HufflenPlancall/cc present in some languages, e.g., Ruby.
Standard ML of New Jersey provides typed continuations,and escape continuations as typed control continuations(being ’a control_cont type).
Haskell ⇐= continuation monad.

17/6/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

Programming languages with continuations

Jean-Michel
HufflenPlancall/cc present in some languages, e.g., Ruby.
Standard ML of New Jersey provides typed continuations,and escape continuations as typed control continuations(being ’a control_cont type).
Haskell ⇐= continuation monad.
Compiling such languages by generating C code—e.g.,
bigloo—a C compiler being in charge of low-level details.

18/6/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

C compiler certified

Jean-Michel
Hufflen
PlanMotivation

Some research projects aim to ensure that C codes arecorrectly put into action.
I Frama-C, developed using OCaml, but not fully proved
yet,Continuation
semantics
ExamplesBridgeScheme/C
Future work

19/7/16

Implementing
EscapeContinuations inC

C compiler certified

Jean-Michel
Hufflen
PlanMotivation

Some research projects aim to ensure that C codes arecorrectly put into action.
I Frama-C, developed using OCaml, but not fully provedyet,
I an attempt to use Coq (CompCert).

20/7/16

Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inCA continuation semantics for C

Jean-Michel
Hufflen
Plan

Functions:

Motivation

mExp : Exp → Envf → Env → State → Ce → (D × State)Continuation
semantics
Exampleswhere:
I State is the program’s state,

BridgeScheme/C
Future work

I Env and Envf are environments,
I Ce = (D × State) → (D × State),
I D is the set of all possible values.

21/8/16

Implementing
EscapeContinuations inC

Example: assignment

Jean-Michel
Hufflen
Plan
Motivation

mExp : Exp → Envf → Env → State → Ce → (D × State)Continuation
semantics
Examples

mExp (assignment(var , e)) ρf ρ s k =let k0 = (v0 , s0 ) 7→ k(v0 , s0 ⊕ [ρ(var ) 7→ v0 ])in mExp e ρf ρ s k0
end

BridgeScheme/C
Future work

22/9/16

Implementing
EscapeContinuations inC

Example: assignment

Jean-Michel
Hufflen
PlanMotivation

mExp : Exp → Envf → Env → State → Ce → (D × State)Continuation
semantics
Examples

mExp (assignment(var , e)) ρf ρ s k =let k0 = (v0 , s0 ) 7→ k(v0 , s0 ⊕ [ρ(var ) 7→ v0 ])in mExp e ρf ρ s k0
end

BridgeScheme/C
Future work

Within such a framework, the future of any computation isalways explicit.

23/9/16

Implementing
EscapeContinuations inC

Functions setjmp/longjmp

Jean-Michel
HufflenPlanmExp : Exp → Envf → Env → State → Ce → (D × State)mExp (setjmp(env )) ρf ρ s k =(0, s ⊕ [ρ(env ) 7→ (k, s)])Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

24/10/16

Implementing
EscapeContinuations inC

Functions setjmp/longjmp

Jean-Michel
HufflenPlanmExp : Exp → Envf → Env → State → Ce → (D × State)mExp (setjmp(env )) ρf ρ s k =(0, s ⊕ [ρ(env ) 7→ (k, s)])Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

mExp (longjmp(env ), e) ρf ρ s k =let (k0 , s0 ) = s(ρ(env ))in mExp e ρf ρ s0 k0
end

25/10/16

Implementing
EscapeContinuations inC

Our framework

Jean-Michel
Hufflen
Plan
Motivation
Continuation
semantics

Showing examples: tree-sum-ep.scm—or tree-sum-ep.sml if astrongly typed language is preferred—and tree-sum.c.

ExamplesBridgeScheme/C
Future work

26/11/16

Implementing
EscapeContinuations inC

Our framework (continued)

Jean-Michel
HufflenPlan

A function launches a computation by means of recursive
auxiliary functions.

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

27/12/16

Implementing
EscapeContinuations inC

Our framework (continued)

Jean-Michel
HufflenPlan

A function launches a computation by means of recursive
auxiliary functions.
These auxiliary functions are not internal, so all thearguments are explicit.

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

28/12/16

Implementing
EscapeContinuations inC

Our framework (continued)

Jean-Michel
HufflenPlan

A function launches a computation by means of recursive
auxiliary functions.
These auxiliary functions are not internal, so all thearguments are explicit.
In particular, one argument of them expresses the way toescape a recursive computation leading to a dead end. For aC program, this is a variable being type jmp_buf.

29/12/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementingEscapeContinuations inC

Our framework (continued)

Jean-Michel
Hufflen
PlanA function launches a computation by means of recursive
auxiliary functions.
These auxiliary functions are not internal, so all thearguments are explicit.
In particular, one argument of them expresses the way toescape a recursive computation leading to a dead end. For aC program, this is a variable being type jmp_buf.
One way to express escaping a computation.

30/12/16

Motivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workImplementing
EscapeContinuations inC

More formally

Jean-MichelHufflen
Plan(call/ec (lambda (exit-0) |{z}. . . ))Motivation
Continuation
semanticsÊvsExamples

if (setjmp(env))...
; else |{z}... ;|{z}escapeÊfunction’sincallC

31/13/16

BridgeScheme/C
Future workImplementing
EscapeContinuations inC

Basic equivalences

Jean-Michel
Hufflen
Plan
Motivation
Continuation
semantics

Between Scheme types and C ones, e.g., integers, trees. . .

ExamplesBridgeScheme/C
Future work

32/14/16

Implementing
EscapeContinuations inC

Our functions

Jean-Michel
HufflenLet f be a Scheme (or Standard ML) function, let x (resp. y )be an element of f ’s domain (resp. codomain); if we denote
the respective implementations in C by C (f ), C (x), C (y ),then:f (x) = y =⇒ C (f )(C (x)) = C (y )PlanMotivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

33/15/16

Implementing
EscapeContinuations inC

Our functions

Jean-Michel
HufflenLet f be a Scheme (or Standard ML) function, let x (resp. y )be an element of f ’s domain (resp. codomain); if we denote
the respective implementations in C by C (f ), C (x), C (y ),then:f (x) = y =⇒ C (f )(C (x)) = C (y )PlanMotivation
Continuation
semantics
ExamplesBridgeScheme/C
Future workHow?

34/15/16

Implementing
EscapeContinuations inC

Our functions

Jean-Michel
HufflenLet f be a Scheme (or Standard ML) function, let x (resp. y )be an element of f ’s domain (resp. codomain); if we denote
the respective implementations in C by C (f ), C (x), C (y ),then:f (x) = y =⇒ C (f )(C (x)) = C (y )PlanMotivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

How? Operational semantics of Scheme and continuation
semantics of C.

35/15/16

Implementing
EscapeContinuations inC

Our functions

Jean-Michel
HufflenLet f be a Scheme (or Standard ML) function, let x (resp. y )be an element of f ’s domain (resp. codomain); if we denote
the respective implementations in C by C (f ), C (x), C (y ),then:f (x) = y =⇒ C (f )(C (x)) = C (y )PlanMotivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

How? Operational semantics of Scheme and continuation
semantics of C.
By induction on the level of recursive calls.

36/15/16

Implementing
EscapeContinuations inC

Our functions

Jean-Michel
HufflenLet f be a Scheme (or Standard ML) function, let x (resp. y )be an element of f ’s domain (resp. codomain); if we denote
the respective implementations in C by C (f ), C (x), C (y ),then:f (x) = y =⇒ C (f )(C (x)) = C (y )PlanMotivation
Continuation
semantics
ExamplesBridgeScheme/C
Future work

How? Operational semantics of Scheme and continuation
semantics of C.
By induction on the level of recursive calls.
Strong induction.

37/15/16

Implementing
EscapeContinuations inCFuture work

Jean-Michel
Hufflen
PlanMotivation
Continuation
semantics

Several ways to escape dead-end computations.

ExamplesBridgeScheme/C
Future work

38/16/16

Implementing
EscapeContinuations inCFuture work

Jean-Michel
Hufflen
Plan
Motivation
Continuation
semantics

Several ways to escape dead-end computations.
Make explicit rules as patterns.

ExamplesBridgeScheme/C
Future work

39/16/16

Implementing
EscapeContinuations inCFuture work

Jean-Michel
Hufflen
Plan
Motivation

Several ways to escape dead-end computations.
Make explicit rules as patterns.
Implementation of C’s continuation semantics using Coq.

Continuation
semantics
ExamplesBridgeScheme/C
Future work

40/16/16

Implementing
EscapeContinuations inC

Future work

Jean-Michel
Hufflen
Plan
Motivation

Several ways to escape dead-end computations.
Make explicit rules as patterns.
Implementation of C’s continuation semantics using Coq.
Writing the complete article ⇐= looking for proof-readers
next spring.

41/16/16

Continuation
semantics
ExamplesBridgeScheme/C
Future work