diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index a9a6cc8..f8e3633 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -237,7 +237,7 @@ match w with \begin{minipage}{0.6\linewidth} \begin{lstlisting} match w with -| p₁|p₂|p₃ -> expr +|p₁ |p₂ |p₃ -> expr \end{lstlisting} \end{minipage} We also support \texttt{when} guards, which are interesting as they @@ -559,8 +559,8 @@ type color = | Red | Blue | Green | Black | White match color with | Red -> print "red" -| Blue -> print "red" -| Green -> print "red" +| Blue -> print "blue" +| Green -> print "green" | _ -> print "white or black" #+END_SRC @@ -751,60 +751,6 @@ existing translators that consists of taking the source and the target * Translation validation of the Pattern Matching Compiler ** 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 following form: @@ -1200,17 +1146,243 @@ Here = 1 In our prototype the source matrix mₛ is defined as follows | 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 an intermediate node with different children sharing the same accessor /a/ 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 -doesn't use a wildcard pattern. -%%% Give example of thing -| Cₛ ::= Leaf bb \vert Switch(a, (Kᵢ → Cᵢ)^{i∈S} , C?) \vert Failure \vert Unreachable -| vₛ ::= K(vᵢ)^{i∈I} \vert n ∈ ℕ -\begin{comment} + +The parametrized grammar $D(\pi, e)$ describes the common structure of +source and decision trees. We use $\pi$ for the \emph{conditions} on +each branch, and $a$ for our \emph{accessors}, which give a symbolic +description of a sub-value of the scrutinee. Source conditions $\pi_S$ +are just datatype constructors; target conditions $\pi_T$ are +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? \end{comment} 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 | (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ -TODO +# TODO - -** 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. -Integer additions and subtractions are simplified in a second pass. +\subsection{From target programs to target decision trees} +# TODO: replace C with D +Symbolic Values during symbolic evaluation have the following form +| vₜ ::= Cell(tag ∈ ℕ, (vᵢ)^{i∈I}) \vert n ∈ ℕ The result of the symbolic evaluation is a target decision tree Cₜ | 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 -| Domain π = { n\vert{}n∈ℕ x n\vert{}n∈Tag⊆ℕ } -Intuitively, the π condition at every branch tells us the set of +Every branch of the decision tree is "constrained" by a domain πₜ that +intuitively tells us the set of 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 possible values that the type of the function can hold. C? is the fallback node of the tree that is taken whenever the value diff --git a/tesi/tesi_unicode.pdf b/tesi/tesi_unicode.pdf deleted file mode 100644 index 6abaa16..0000000 Binary files a/tesi/tesi_unicode.pdf and /dev/null differ diff --git a/todo.org b/todo.org index d46db30..0b294a9 100644 --- a/todo.org +++ b/todo.org @@ -1,4 +1,4 @@ -* TODO VPC [21/23] +* TODO VPC [23/24] - [X] Controlla good latex - [X] Uppaal muovi cartella file - [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 quando coperta da p-semiflows - [X] Vedi bisimulazione ed equivalenze in teoria analisi -- [ ] Che significa urgente in uppaal? -- [ ] Uppaal: x = 0 come guardia, non == -- [-] Teoria [1/13] +- [X] Che significa urgente in uppaal? +- [X] Uppaal: x = 0 come guardia, non == +- [-] Teoria [8/21] + - [X] Come metti a parole \to ? - [ ] Hierarchy of equivalences - [ ] algebra.extra.lucca: internal/external choices - [ ] Observer e testing equivalence - - [ ] Vedi bene legge conservazione token + - [X] Vedi bene legge conservazione token - [ ] Vedi bene fairness, liveness come formule? - [ ] Vedi da relazioni procedure dimostrazione deadlock - [ ] Impara equivalenze come le spiega lei @@ -26,15 +27,24 @@ - [ ] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL - [ ] CTL e LTL: set operatori minimo per derivare altri - [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 + - [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] Spiega p-t-semiflows analysis: deadlock e liveness, boundness - - [X] sulle slide, quando si chiede come deve decidere il master - - [X] Sistema screenshots di GSPN non tagliati - - [X] Controlla riduzione se hai fuso posti con archi uscenti - - [X] Rifai la riduzione e controlla fusione con archi uscenti - - [X] chiedi Daniel riduzione + + [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness + + [X] sulle slide, quando si chiede come deve decidere il master + + [X] Sistema screenshots di GSPN non tagliati + + [X] Controlla riduzione se hai fuso posti con archi uscenti + + [X] Rifai la riduzione e controlla fusione con archi uscenti + + [X] chiedi Daniel riduzione - [X] rete E, F -> Controlla sia finito - [X] Analisi [27/27] - [X] clearpage su ultime immagini @@ -98,6 +108,9 @@ * Tesi [3/9] - [ ] 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] Gatti: inglese - [X] Gatti: Coppo mio relatore @@ -122,5 +135,10 @@ - [ ] Trimming e resto: mi sa che usi left e right male - [ ] Spiega perche` trimming non simmetrico - [ ] 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!