Appendix o Endange ed by he Language Bu Sa ed by he
Compile : Robus Sa e y ia Seman ic Back-T ansla ion
NIKLAS MÜCK,MPI-SWS, Ge many
AÏNA LINN GEORGES,MPI-SWS, Ge many
DEREK DREYER,MPI-SWS, Ge many
DEEPAK GARG,MPI-SWS, Ge many
MICHAEL SAMMLER,Ins i u e o Science and Technology Aus ia (ISTA), Aus ia
A De ini ion o UNIV
This sec ion p esen s he de ails o he de ini ion o
UNIV
ha o e app oxima es all
Cap
p og ams.
UNIV
is de ined as a seman ic DimSum module based on p e- and pos condi ions, simila o
SIM
.
The de ini ion is a li le mo e in ol ed han he de ini ion o
SIM
because ou a ge language
Cap
is less abs ac and has a sepa a e s ack. I is inspi ed by p io wo k on uni e sal con ac s o
capabili y machines [3,4,1,2].
Fi s , we need o de ine a no ion o shadow s acks
shd ∈ShadowS ack
ha consis o shadow
ames
s ∈ShadowF ame
(Fig. 1). These shadows s acks a e necessa y since he ope a ional
seman ic o
Cap
can euse s ack ames and hus jus he dep h o a s ack ame does no uniquely
iden i y i . Thus, he shadow s acks associa e ghos iden i ie s
𝜄∈Ghos Id
wi h he (physical)
s ack. This associa ion is encoded by he
shd ∼s
ela ion ha s a es ha he shadow s ack
shd
and
physical s ack
s
ag ee. We use he ghos ids in
capP op
o de ining poin s- o p edica es o he
s ack.
Addi ionally, we need o ensu e ha
UNIV
does no b eak well-b acke ed con ol low, i.e., does
no skip s ack ames wi hou e u ning. Fo ha we de ine a s epping ela ion o alid in e nal
ope a ions o a (shadow) s ack
→
ha a p og am wi h add ess space
A
can do. In pa icula , i can
only e u n i he e u n and con inue exec uing i he e u n add ess is wi hin
A
(see shd- e ). We
w i e →*as he e lexi e ansi i e closu e o he ela ion.
Nex , we de ine a se o (pu e)
Cap
language in a ian s
LangIn
ha a e necessa y o ensu e
capabili y sa e y o
Cap
: The e mus be no dangling poin e s, he s ack is di ec ed, and he heap
con ains no s ack poin e s.
Wi h ha we can inally de ine
UNIV
in Fig. 2. Simila o he de ini ion o
SIM
,
in
𝐿,shd
UNIV(s,m)
con ains he s a e in e p e a ions ha ie he sepa a ion logic o he cu en physical s a e o he
s ack and heap. No e ha he s a e in e p e a ion o he s ack is pa ame ized o e he cu en
shadow s ack o he mapping o physical s ack ids and ghos ids. Again i con ains he global iew
o low capabili ies and ensu es ha hey a e ansi i ely low.
𝐿
a se o al eady alloca ed capabili ies
ha a e no low. (This se is used in he seman ic back- ansla ion p oo ). I can be chosen in he
p econdi ion o UNIV and is p ese ed in he pos condi ion.
The
p eUNIV
and
pos UNIV
en o ce ha all egis e s only con ain
low
alues and he
in UNIV
and
LangIn
hold o he cu en s a e passed by he
Jump
-e en . The
UNIV
keeps as s a e he las
Au ho s’ Con ac In o ma ion: Niklas Mück, MPI-SWS, Saa land In o ma ics Campus, Ge many, [email protected] g;
Aïna Linn Geo ges, MPI-SWS, Saa land In o ma ics Campus, Ge many, algeo [email protected] g; De ek D eye , MPI-SWS,
Saa land In o ma ics Campus, Ge many, d eye @mpi-sws.o g; Deepak Ga g, MPI-SWS, Saa land In o ma ics Campus,
Ge many, [email protected] g; Michael Sammle , Ins i u e o Science and Technology Aus ia (ISTA), Klos e neubu g, Aus ia,
[email p o ec ed].
2018. ACM 2475-1421/2018/1-ART1
h ps://doi.o g/
P oc. ACM P og am. Lang., Vol. 1, No. CONF, A icle 1. Publica ion da e: Janua y 2018.
1:2 Niklas Mück, Aïna Linn Geo ges, De ek D eye , Deepak Ga g, and Michael Sammle
ShadowF ame ∋s ≜ B × P(Z) × Wo d ×HeapCap ×op ion(Ghos Id)
ShadowS ack ∋shd ≜(L (ShadowF ame),P(Ghos Id))
shd ∼s≜shd.1=s.1∧shd.2=dom(s.2) ∧ shd.3=s.3∧shd.4=s.4
shd-call
e .a−1∈A
(shd,I) →A(shd
+
+
( alse,∅,sp, e ,None),I⊎{𝜄})
shd- e
e .a∈A
(shd
+
+
(_,_,_, e ,_),I) →A(shd,I)
shd-alloc
(shd
+
+
( alse,∅,sp, e ,None),I) →A(shd
+
+
( ue,d,sp, e ,Some(𝜄)),I⊎{𝜄})
LangIn ( ,m,s)≜NoDanglingPoin e ( ,m,s) ∧ Di ec ed(s) ∧ NoS kPoin e (m)
Fig. 1. Language In a ian s o Cap
in
𝐿,shd
UNIV(s,m)≜SIshd
s k (s) ∗ SIheap(m) ∗ ∃𝐿⊎
𝐿. LowAu h(𝐿) ∗
∗
c∈𝐿
∃w.c↦→m/sw∗lowshd(w)
p eA?,E!
UNIV (e,shd,call_s k)⇀(shd′,call_s k′,
𝐿)≜∃ ,m,s.in
𝐿,shd′
UNIV (s,m) ∗
∗
w∈
lowshd′(w)
∗LangIn ( ,m,s) ∗ e=Jump?( ,m,s)∗shd′∼s∗pc( ).a∈ A?∗
𝐿⊆I(shd′)
∗ ∃A⊎ A?.shd →*Ashd′∗ ∃shdp e e .shd′=shdp e
+
+
(_,_,_, e ,_) ∗ e .a∉A?
∗call_s k′=shd′
?:: call_s k
∨∃shdp e.shd →*Ashdp e ∗shdp e =shd′
+
+
(_,_,sp( ),pc( ),_)
∗call_s k =shdp e!::call_s k′
pos A?,E!
UNIV (e,shd′,call_s k′)↽(shd,call_s k,
𝐿)≜∃ ,m,s.in
𝐿,shd′
UNIV (s,m) ∗
∗
w∈
lowshd′(w)
∗LangIn ( ,m,s) ∗ e=Jump!( ,m,s)∗shd′∼s∗pc( ).a∉A?
shd →*A?shd′∗ ∃shdp e e .shd′=shdp e
+
+
(_,_,_, e ,_) ∗ e .a∈ A?
∗call_s k′=shd′
!:: call_s k
∨∃shdp e.shd →*Ashdp e ∗shdp e =shd′
+
+
(_,_,sp( ),pc( ),_)
∗call_s k =shdp e?::call_s k′
Fig. 2. De ini ion o UNIV
shd
i saw. In he p e-condi ion i is gi en a
shd′∼s
and hen assumes ha i was de i ed by
only alid ope a ions
→*A
by on an ex e nal add ess space
A⊎ A?
. In he pos -condi ion i p o es
acco dingly ha he new
shd′
was de i ed by he old one only by ope a ions wi hin
A?
. Jumps
ha we e emi ed by he
e
-ins uc ion, do a non-local ope a ion on he s ack ha is he e o e
no cap u ed by
→*
and ea ed sepa a ely in he
p eUNIV
and
pos UNIV
. Addi ionally, i is ensu ed
ha he
sp
and
pc
s o ed on he s ack a e co ec ly loaded back in o he egis e s. In o de o mo e
P oc. ACM P og am. Lang., Vol. 1, No. CONF, A icle 1. Publica ion da e: Janua y 2018.
Appendix o Endange ed by he Language Bu Sa ed by he Compile : Robus Sa e y ia Seman ic Back-T ansla ion 1:3
con inen ly asse ha well-b acke edness implies ha he
shd
a he ime o a call is es o ed a he
ime o a e u n,
UNIV
keeps a lis o open calls
call_s k
in i s s a e oge he wi h he in o ma ion
whe e he call came om.
Re e ences
[1]
Aïna Linn Geo ges, A maël Guéneau, Thomas Van S ydonck, Amin Timany, Alix T ieu, Sande Huyghebae , Dominique
De iese, and La s Bi kedal. 2021. E icien and p o able local capabili y e oca ion using unini ialized capabili ies.
P oc. ACM P og am. Lang. 5, POPL (2021), 1–30. doi:10.1145/3434287
[2]
Aïna Linn Geo ges, Alix T ieu, and La s Bi kedal. 2022. Le emps des ce ises: e icien empo al s ack sa e y on capabili y
machines using di ec ed capabili ies. P oc. ACM P og am. Lang. 6, OOPSLA1 (2022), 1–30.
[3]
Lau Sko s engaa d, Dominique De iese, and La s Bi kedal. 2020. Reasoning abou a Machine wi h Local Capabili ies:
P o ably Sa e S ack and Re u n Poin e Managemen . ACM T ans. P og am. Lang. Sys . 42, 1 (2020), 5:1–5:53. doi:10.
1145/3363519
[4]
Lau Sko s engaa d, Dominique De iese, and La s Bi kedal. 2021. S kTokens: En o cing well-b acke ed con ol low
and s ack encapsula ion using linea capabili ies. J. Func . P og am. 31 (2021), e9. doi:10.1017/S095679682100006X
P oc. ACM P og am. Lang., Vol. 1, No. CONF, A icle 1. Publica ion da e: Janua y 2018.
