bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

small changes related to abstract

Browse source
This commit is contained in:
Francesco Mecca 2020-05-27 18:49:35 +02:00
parent 3733c6ef5a
commit 286cda4043
3 changed files with 277 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

355
tesi/tesi_unicode.org
View file

@ -559,8 +559,8 @@ type color = | Red | Blue | Green | Black | White
match color with match color with
| Red -> print "red" | Red -> print "red"
| Blue -> print "red" | Blue -> print "blue"
| Green -> print "red" | Green -> print "green"
| _ -> print "white or black" | _ -> print "white or black"
#+END_SRC #+END_SRC
@ -751,60 +751,6 @@ existing translators that consists of taking the source and the target
* Translation validation of the Pattern Matching Compiler * Translation validation of the Pattern Matching Compiler
** Source program ** Source program
Our algorithm takes as its input a source program and translates it
into an algebraic data structure which type we call /decision_tree/.
#+BEGIN_SRC
type decision_tree =
| Unreachable
| Failure
| Leaf of source_expr
| Guard of source_blackbox * decision_tree * decision_tree
| Switch of accessor * (constructor * decision_tree) list * decision_tree
#+END_SRC
Unreachable, Leaf of source_expr and Failure are the terminals of the three.
We distinguish
- Unreachable: statically it is known that no value can go there
- Failure: a value matching this part results in an error
- Leaf: a value matching this part results into the evaluation of a
source black box of code
Our algorithm doesn't support type-declaration-based analysis
to know the list of constructors at a given type.
Let's consider some trivial examples:
| function true -> 1
is translated to
|Switch ([(true, Leaf 1)], Failure)
while
| function
| \vert{} true -> 1
| \vert{} false -> 2
will be translated to
|Switch ([(true, Leaf 1); (false, Leaf 2)])
It is possible to produce Unreachable examples by using
refutation clauses (a "dot" in the right-hand-side)
|function
|\vert{} true -> 1
|\vert{} false -> 2
|\vert{} _ -> .
that gets translated into
| Switch ([(true, Leaf 1); (false, Leaf 2)], Unreachable)
We trust this annotation, which is reasonable as the type-checker
verifies that it indeed holds.
Guard nodes of the tree are emitted whenever a guard is found. Guards
node contains a blackbox of code that is never evaluated and two
branches, one that is taken in case the guard evaluates to true and
the other one that contains the path taken when the guard evaluates to
true.
\begin{comment}
[ ] Finisci con Switch
[ ] Spiega del fallback
\end{comment}
The source code of a pattern matching function has the The source code of a pattern matching function has the
following form: following form:
@ -1200,17 +1146,243 @@ Here = 1
In our prototype the source matrix mₛ is defined as follows In our prototype the source matrix mₛ is defined as follows
| SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I} | SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I}
Source matrices are used to build source decision trees Cₛ. ** Target translation
The target program of the following general form is parsed using a parser
generated by Menhir, a LR(1) parser generator for the OCaml programming language.
Menhir compiles LR(1) a grammar specification, in this case a subset
of the Lambda intermediate language, down to OCaml code.
This is the grammar of the target language (TODO: check menhir grammar)
| start ::= sexpr
| sexpr ::= variable \vert{} string \vert{} "(" special_form ")"
| string ::= "\"" identifier "\"" ;; string between doublequotes
| variable ::= identifier
| special_form ::= let\vert{}catch\vert{}if\vert{}switch\vert{}switch-star\vert{}field\vert{}apply\vert{}isout
| let ::= "let" assignment sexpr ;; (assignment sexpr)+ outside of pattern match code
| assignment ::= "function" variable variable+ ;; the first variable is the identifier of the function
| field ::= "field" digit variable
| apply ::= ocaml_lambda_code ;; arbitrary code
| catch ::= "catch" sexpr with sexpr
| with ::= "with" "(" label ")"
| exit ::= "exit" label
| switch-star ::= "switch*" variable case*
| switch::= "switch" variable case* "default:" sexpr
| case ::= "case" casevar ":" sexpr
| casevar ::= ("tag"\vert{}"int") integer
| if ::= "if" bexpr sexpr sexpr
| bexpr ::= "(" ("!="\vert{}"=="\vert{}">="\vert{}"<="\vert{}">"\vert{}"<") sexpr digit \vert{} field ")"
| label ::= integer
The prototype doesn't support strings.
The AST built by the parser is traversed and evaluated by the symbolic
execution engine.
Given that the target language supports jumps in the form of "catch - exit"
blocks the engine tries to evaluate the instructions inside the blocks
and stores the result of the partial evaluation into a record.
When a jump is encountered, the information at the point allows to
finalize the evaluation of the jump block.
In the environment the engine also stores bindings to values and
functions.
For performance reasons the compiler performs integer addition and
subtraction on variables that appears inside a /switch/ expression in
order to have values always start from 0.
Let's see an example of this behaviour:
#+BEGIN_SRC
let f x = match x with
| 3 -> "3"
| 4 -> "4"
| 5 -> "5"
| 6 -> "6"
| _ -> "_"
#+END_SRC
#+BEGIN_SRC
(setglobal Prova!
(let
(f/80 =
(function x/81[int]
(catch
(let (switcher/83 =a (-3+ x/81))
(if (isout 3 switcher/83) (exit 1)
(switch* switcher/83
case int 0: "3"
case int 1: "4"
case int 2: "5"
case int 3: "6")))
with (1) "_")))
(makeblock 0 f/80)))
#+END_SRC
The prototype takes into account such transformations and at the end
of the symbolic evaluation it traverses the result in order to "undo"
such optimization and have accessors of the variables match their
intended value directly.
** Decision Trees
For the source language we use Source matrices to build source
decision trees Cₛ,
while in the case of the target language the decision tree Cₜ is the
result of the symbolic execution on the lambda code.
We give the following definitions.
| Source and target programs: tₛ and tₜ
| Source and target expressions: eₛ and eₜ
A source program $t_S$ is a list of pattern-matching
clauses (with an optional \texttt{when}-guard) of the form
\lstinline{| $p$ (when $e_S$)? -> $e_S$}, and a target program $t_T$
is a series of control-flow conditionals (\texttt{if, switch,
Match\_failure, catch, exit}), value access (\texttt{field}),
variable bindings (\texttt{let}) and comparison operators in Lambda
code, with arbitrary Lambda-code expressions $e_T$ at the leaves.
We assume given an equivalence relation $\erel {e_S} {e_T}$ on
expressions (that are contained in the leaves of the decision trees).
In our translation-validation setting, it suffices to
relate each source expression to its compiled form -- the compiler
computes this relation. We have to lift this relation on leaves
into an equivalence procedure for (pattern-matching) programs.
We already defined what it means to run a value vₛ against a program
tₛ:
| tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥
| tₛ(vₛ) = { Absurd if bb_{i₀} = . (refutation clause)
| \quad \quad \quad \quad \quad Match (σ, bb_{i₀}) otherwise
| \quad \quad \quad \quad \quad where iₒ = min{i \vert{} pᵢ(vₛ) ≠ ⊥}
and simmetrically, to run a value vₜ against a target program tₜ:
# TODO t_t
Starting from this we can define a
a relation $\vrel {v_S} {v_T}$ to relate a source to a target value
in terms of equivalence between the two results:
\begin{mathpar}
\erel {e_S} {e_T} \; (\text{\emph{assumed}})
t_S(v_S),\ t_T(v_T),\ \vrel {v_S} {v_T} \; (\text{\emph{omitted}})
\resrel {r_S} {r_T}, \runrel {R_S} {R_T} \; (\text{\emph{simple}})
\\
\begin{array}{l@{~}r@{~}r@{~}l}
\text{\emph{environment}} & \sigma(v)
& \bnfeq & [x_1 \mapsto v_1, \dots, v_n \mapsto v_n] \\
\text{\emph{closed term}} & \cle(v)
& \bnfeq & (\sigma(v), e) \\
\end{array}
\quad
\begin{array}{l@{~}r@{~}r@{~}l}
\text{\emph{matching result}} & r(v)
& \bnfeq & \NoMatch \bnfor \Match {\cle(v)} \\
\text{\emph{matching run}} & R(v)
& \bnfeq & (\cle(v)_1, \dots, \cle(v)_n), r(v) \\
\end{array}
\\
\infer
{\forall x,\ \vrel {\sigma_S(x)} {\sigma_T(x)}}
{\envrel {\sigma_S} {\sigma_T}}
\infer
{\envrel {\sigma_S} {\sigma_T} \\ \erel {e_S} {e_T}}
{\clerel {(\sigma_S, e_S)} {(\sigma_T, e_T)}}
\infer
{\forall {\vrel {v_S} {v_T}},\quad \runrel {t_S(v_S)} {t_T(v_T)}}
{\progrel t_S t_T}
\end{mathpar}
This relation captures our knowledge of the
OCaml value representation, for example it relates the empty list
constructor \texttt{[]} to $\Int 0$. We can then define \emph{closed}
expressions $\cle$, pairing a (source or target) expression with the
environment $\sigma$ captured by a program, and what it means to
``run'' a value against a program or a decision, written $t(v)$ and
$D(v)$, which returns a trace $(\cle_1, \dots, \cle_n)$ of the
executed guards and a \emph{matching result} $r$.
Once formulated in this way, our equivalence algorithm must check the
natural notion of input-output equivalence for matching programs,
captured by the relation $\progrel {t_S} {t_T}$.
# TODO eq_muovi
\subsection{Grammar of the decision trees}
A decision tree is defined as either a Leaf, a Failure terminal or A decision tree is defined as either a Leaf, a Failure terminal or
an intermediate node with different children sharing the same accessor /a/ an intermediate node with different children sharing the same accessor /a/
and an optional fallback. and an optional fallback.
Failure is emitted only when the patterns don't cover the whole set of
possible input values /S/. The fallback is not needed when the user The parametrized grammar $D(\pi, e)$ describes the common structure of
doesn't use a wildcard pattern. source and decision trees. We use $\pi$ for the \emph{conditions} on
%%% Give example of thing each branch, and $a$ for our \emph{accessors}, which give a symbolic
| Cₛ ::= Leaf bb \vert Switch(a, (Kᵢ → Cᵢ)^{i∈S} , C?) \vert Failure \vert Unreachable description of a sub-value of the scrutinee. Source conditions $\pi_S$
| vₛ ::= K(vᵢ)^{i∈I} \vert n ∈ ℕ are just datatype constructors; target conditions $\pi_T$ are
\begin{comment} arbitrary sets of possible immediate-integer or block-tag values.
%
\begin{mathpar}
\begin{array}{l@{~}r@{~}r@{~}l}
\text{\emph{decision trees}} & D(\pi, e)
& \bnfeq & \Leaf {\cle(a)} \\
& & \bnfor & \Failure \\
& & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb \\
& & \bnfor & \Guard {\cle(a)} {D_0} {D_1} \\
& & \bnfor & Unreachable \\
\text{\emph{accessors}} & a
& \bnfeq & \Root \;\bnfor\; a.n \quad (n \in \mathbb{N}) \\
\end{array}
\quad
\begin{array}{l}
\pi_S : \text{datatype constructors}
\\
\pi_T \subseteq \{ \Int n \mid n \in \mathbb{Z} \}
\uplus \{ \Tag n \mid n \in \mathbb{N} \}
\\[1em]
a(v_S), a(v_T), D_S(v_S), D_T(v_T) \quad (\text{\emph{omitted})}
\end{array}
\end{mathpar}
The tree $\Leaf \cle$ returns a leaf expression $e$ in a captured
environment $\sigma$ mapping variables to accessors.
%
$\Failure$ expresses match failure, when no clause matches the input
value.
%
$\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$
for every head constructor that appears in the pattern matching
clauses, and a fallback case for the constructors.
%
$\Guard \cle {D_0} {D_1}$ represents a \texttt{when}-guard on a closed
expression $\cle$, expected to be of boolean type, with sub-trees
$D_0$ for the \texttt{true} case and $D_1$ for the \texttt{false}
case.
We write $a(v)$ for the sub-value of the (source or target) value $v$
that is reachable at the accessor $a$, and $D(v)$ for the result of
running a value $v$ against a decision tree $D$; this results in
a (source or target) matching run $R(v)$, just like running the value
against a program.
\subsection{From source programs to decision trees}
Let's consider some trivial examples:
| function true -> 1
is translated to
|Switch ([(true, Leaf 1)], Failure)
while
| function
| \vert{} true -> 1
| \vert{} false -> 2
will be translated to
|Switch ([(true, Leaf 1); (false, Leaf 2)])
It is possible to produce Unreachable examples by using
refutation clauses (a "dot" in the right-hand-side)
|function
|\vert{} true -> 1
|\vert{} false -> 2
|\vert{} _ -> .
that gets translated into
| Switch ([(true, Leaf 1); (false, Leaf 2)], Unreachable)
We trust this annotation, which is reasonable as the type-checker
verifies that it indeed holds.
We'll see that while we can build Unreachable nodes from source
programs, in the lambda target there isn't a construct equivalent to the refutation clause.
Guard nodes of the tree are emitted whenever a guard is found. Guards
node contains a blackbox of code that is never evaluated and two
branches, one that is taken in case the guard evaluates to true and
the other one that contains the path taken when the guard evaluates to
true.
Are K and Here clear here? Are K and Here clear here?
\end{comment} \end{comment}
We say that a translation of a source program to a decision tree We say that a translation of a source program to a decision tree
@ -1384,55 +1556,20 @@ In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)
we have to prove that we have to prove that
| (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ | (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ
TODO # TODO
\subsection{From target programs to target decision trees}
** Target translation # TODO: replace C with D
Symbolic Values during symbolic evaluation have the following form
The target program of the following general form is parsed using a parser | vₜ ::= Cell(tag ∈ ℕ, (vᵢ)^{i∈I}) \vert n ∈ ℕ
generated by Menhir, a LR(1) parser generator for the OCaml programming language.
Menhir compiles LR(1) a grammar specification, in this case a subset
of the Lambda intermediate language, down to OCaml code.
This is the grammar of the target language (TODO: check menhir grammar)
| start ::= sexpr
| sexpr ::= variable \vert{} string \vert{} "(" special_form ")"
| string ::= "\"" identifier "\"" ;; string between doublequotes
| variable ::= identifier
| special_form ::= let\vert{}catch\vert{}if\vert{}switch\vert{}switch-star\vert{}field\vert{}apply\vert{}isout
| let ::= "let" assignment sexpr ;; (assignment sexpr)+ outside of pattern match code
| assignment ::= "function" variable variable+ ;; the first variable is the identifier of the function
| field ::= "field" digit variable
| apply ::= ocaml_lambda_code ;; arbitrary code
| catch ::= "catch" sexpr with sexpr
| with ::= "with" "(" label ")"
| exit ::= "exit" label
| switch-star ::= "switch*" variable case*
| switch::= "switch" variable case* "default:" sexpr
| case ::= "case" casevar ":" sexpr
| casevar ::= ("tag"\vert{}"int") integer
| if ::= "if" bexpr sexpr sexpr
| bexpr ::= "(" ("!="\vert{}"=="\vert{}">="\vert{}"<="\vert{}">"\vert{}"<") sexpr digit \vert{} field ")"
| label ::= integer
The prototype doesn't support strings.
The AST built by the parser is traversed and evaluated by the symbolic
execution engine.
Given that the target language supports jumps in the form of "catch - exit"
blocks the engine tries to evaluate the instructions inside the blocks
and stores the result of the partial evaluation into a record.
When a jump is encountered, the information at the point allows to
finalize the evaluation of the jump block.
In the environment the engine also stores bindings to values and
functions.
Integer additions and subtractions are simplified in a second pass.
The result of the symbolic evaluation is a target decision tree Cₜ The result of the symbolic evaluation is a target decision tree Cₜ
| Cₜ ::= Leaf bb \vert Switch(a, (πᵢ → Cᵢ)^{i∈S} , C?) \vert Failure | Cₜ ::= Leaf bb \vert Switch(a, (πᵢ → Cᵢ)^{i∈S} , C?) \vert Failure
| vₜ ::= Cell(tag ∈ ℕ, (vᵢ)^{i∈I}) \vert n ∈ ℕ Every branch of the decision tree is "constrained" by a domain πₜ that
Every branch of the decision tree is "constrained" by a domain intuitively tells us the set of
| Domain π = { n\vert{}n∈ℕ x n\vert{}n∈Tag⊆ℕ }
Intuitively, the π condition at every branch tells us the set of
possible values that can "flow" through that path. possible values that can "flow" through that path.
π conditions are refined by the engine during the evaluation; at the | Domain π = { n\vert{}n∈ℕ x n\vert{}n∈Tag⊆ℕ }
# TODO: copy the definition from above
πₜ conditions are refined by the engine during the evaluation; at the
root of the decision tree the domain corresponds to the set of root of the decision tree the domain corresponds to the set of
possible values that the type of the function can hold. possible values that the type of the function can hold.
C? is the fallback node of the tree that is taken whenever the value C? is the fallback node of the tree that is taken whenever the value

BIN
tesi/tesi_unicode.pdf
View file

Binary file not shown.

42
todo.org
View file

@ -1,4 +1,4 @@
* TODO VPC [21/23] * TODO VPC [23/24]
- [X] Controlla good latex - [X] Controlla good latex
- [X] Uppaal muovi cartella file - [X] Uppaal muovi cartella file
- [X] Rimuovi "Contents" da ogni .org - [X] Rimuovi "Contents" da ogni .org
@ -12,13 +12,14 @@
- [X] spiega nelle relazioni che bounded se RS finito - [X] spiega nelle relazioni che bounded se RS finito
- [X] spiega nelle relazioni che bounded quando coperta da p-semiflows - [X] spiega nelle relazioni che bounded quando coperta da p-semiflows
- [X] Vedi bisimulazione ed equivalenze in teoria analisi - [X] Vedi bisimulazione ed equivalenze in teoria analisi
- [ ] Che significa urgente in uppaal? - [X] Che significa urgente in uppaal?
- [ ] Uppaal: x = 0 come guardia, non == - [X] Uppaal: x = 0 come guardia, non ==
- [-] Teoria [1/13] - [-] Teoria [8/21]
- [X] Come metti a parole \to ?
- [ ] Hierarchy of equivalences - [ ] Hierarchy of equivalences
- [ ] algebra.extra.lucca: internal/external choices - [ ] algebra.extra.lucca: internal/external choices
- [ ] Observer e testing equivalence - [ ] Observer e testing equivalence
- [ ] Vedi bene legge conservazione token - [X] Vedi bene legge conservazione token
- [ ] Vedi bene fairness, liveness come formule? - [ ] Vedi bene fairness, liveness come formule?
- [ ] Vedi da relazioni procedure dimostrazione deadlock - [ ] Vedi da relazioni procedure dimostrazione deadlock
- [ ] Impara equivalenze come le spiega lei - [ ] Impara equivalenze come le spiega lei
@ -26,15 +27,24 @@
- [ ] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL - [ ] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL
- [ ] CTL e LTL: set operatori minimo per derivare altri - [ ] CTL e LTL: set operatori minimo per derivare altri
- [X] Manca CTL* ? - [X] Manca CTL* ?
- [ ] Pstate? - [X] Pstate? stato che appartiene al linguaggio (o set di label)
della struttura di Kripke
- [ ] BDD e decision diagrams, tutto Amparore - [ ] BDD e decision diagrams, tutto Amparore
- [X] Galla`: TCTL z in \phi
- [X] Slide 44 TCTL? reset?
- [ ] Slides 49-50 di TCTL
- [X] Equivalenza clock. Davvero mantissa e parte frazionaria?
- [X] Galla`: che devo dire sulle WN?
- [ ] Rivedi WN
- [ ] Perche` sono utili gli t-semiflussi? PN consistente?
- [ ] Assicurati di sapere le sigle
- [X] rete A, b, c, d [6/6] - [X] rete A, b, c, d [6/6]
- [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness + [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
- [X] sulle slide, quando si chiede come deve decidere il master + [X] sulle slide, quando si chiede come deve decidere il master
- [X] Sistema screenshots di GSPN non tagliati + [X] Sistema screenshots di GSPN non tagliati
- [X] Controlla riduzione se hai fuso posti con archi uscenti + [X] Controlla riduzione se hai fuso posti con archi uscenti
- [X] Rifai la riduzione e controlla fusione con archi uscenti + [X] Rifai la riduzione e controlla fusione con archi uscenti
- [X] chiedi Daniel riduzione + [X] chiedi Daniel riduzione
- [X] rete E, F -> Controlla sia finito - [X] rete E, F -> Controlla sia finito
- [X] Analisi [27/27] - [X] Analisi [27/27]
- [X] clearpage su ultime immagini - [X] clearpage su ultime immagini
@ -98,6 +108,9 @@
* Tesi [3/9] * Tesi [3/9]
- [ ] Rivedere inference rules di Gabriel e aggiustarle con le mie - [ ] Rivedere inference rules di Gabriel e aggiustarle con le mie
- [ ] Definizione di First(x_i): serve?
- [ ] Equivalenza R_s R_T (run)
- [ ] TODO t_t
- [X] segreteria: tesi inglese - [X] segreteria: tesi inglese
- [X] Gatti: inglese - [X] Gatti: inglese
- [X] Gatti: Coppo mio relatore - [X] Gatti: Coppo mio relatore
@ -122,5 +135,10 @@
- [ ] Trimming e resto: mi sa che usi left e right male - [ ] Trimming e resto: mi sa che usi left e right male
- [ ] Spiega perche` trimming non simmetrico - [ ] Spiega perche` trimming non simmetrico
- [ ] Spiega meglio le guards on equivalence checking - [ ] Spiega meglio le guards on equivalence checking
- [ ] t_T e t_S o t_t e t_s???
- [ ] TODO eq_muovi : si parla di eq checking, forse non li`
- [ ] Gabriel: quello che penso sulle equivalenze omesse e` giusto?
- [ ] Cambia le C di constraint tree in D
- [ ] TODO on the org file
HALP HALP
HALP! HALP!