Changeset 3348
 Timestamp:
 Jun 13, 2013, 1:22:56 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec2.tex
r3347 r3348 92 92 diag/.style={row sep={11mm,between origins}, 93 93 column sep={11mm,between origins}, 94 every node/.style={draw, is other}}, 94 every node/.style={execute at begin node=$, execute at end node=$}, 95 % every node/.style={draw, is other}, 96 }, 95 97 small vgap/.style={row sep={7mm,between origins}}, 96 small gap/.style={row sep={7mm,between origins},column sep={7mm,between origins}}, 98 small hgap/.style={column sep={7mm,between origins}}, 99 small gap/.style={small vgap, small hgap}, 97 100 % for article, maybe temporary 98 101 is jump/.style=is other, … … 695 698 where $\Functions$ is the set of names of functions that can occur in the 696 699 program, $\Labels$ is a set of labels disjoint from $\Functions$ 697 and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. 700 and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. Moreover there 701 is an injective function $\ell : \Functions \to \Labels$ that tells the 702 starting label of the body of each function, and $\ell(\Functions)\subseteq \Labels$ 703 denotes the image of this function. 698 704 The transition function is defined as $s_1 \to[o] s_2$ if 699 705 $s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \Functions$ if … … 715 721 \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a 716 722 label $L$ and a $k\ge i+2$ such that 717 $s_{i+1} \to[ L] s_{i+2} \To s_k \to[RET] s_{k+1}$, with723 $s_{i+1} \to[\ell(f)] s_{i+2} \To s_k \to[RET] s_{k+1}$, with 718 724 $s_i \ar s_{k+1}$. 719 In other words, $s_{i+1}$ must start execution with an \verb+EMIT $L$+725 In other words, $s_{i+1}$ must start execution with \verb+EMIT $\ell(f)$+ 720 726 and then continue with a structured fragment returning control 721 727 to the instruction immediately following the call. … … 723 729 with a label emission statement, and every function 724 730 call must converge yielding back control just after it. 731 \item For every $i$ and $f$, if $s_{i+1}\to[\ell(f)]s_{i+2}$ then 732 $s_i\to[f]s_{i+1}$. This is a technical condition needed to ensure that 733 labels associated with functions always follow a call. 725 734 \item The number of $RET$'s in the fragment is equal to the number of 726 735 calls, i.e.\ the number of observables in $\Functions$. This, together with … … 732 741 live code must start with a label emission. 733 742 \end{enumerate} 734 735 Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ be an 743 One might wonder why $f$ and $\ell(f)$, that aways appear in this order, are not 744 collapsed into a single observable. This would indeed simplify some aspects of 745 the formalisation, but has the problem of misassagning the cost of calls, which would 746 fall under the associated label. As different call instructions with different costs 747 are possible, this is not acceptable. 748 749 Let $T = s_0 \to[o_0] s_1 \ldots \to[o_n] s_{n+1}$ be an 736 750 execution fragment. The \emph{weak trace} $T$ associated to $T$ is the 737 751 subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_n$ obtained dropping … … 739 753 740 754 Let $k$ be a cost model that maps observables actions to any commutative cost 741 monoid (e.g. natural numbers). We extend the domain of $k$ to weak traces742 by posing $k( \mathcal{T}) = \Sigma_{o \in \mathcal{T}} k(o)$.755 monoid (e.g. natural numbers). We extend the domain of $k$ to fragments 756 by posing $k(T) = \Sigma_{o \in T} k(o)$. 743 757 744 758 The labelling approach is based on the idea that the execution cost of … … 1391 1405 % as_after_return s2_pre s2_ret. 1392 1406 % \end{alltt} 1393 1394 1407 \begin{figure} 1395 1408 \centering 1396 \begin{tabular}{@{}c@{}c@{}c@{}}1397 1409 % \begin{subfigure}{.475\linewidth} 1398 1410 % \centering … … 1415 1427 % \end{subfigure} 1416 1428 % & 1417 \begin{subfigure}{.25\linewidth}1418 1429 \centering 1419 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1420 every label/.style=overlay, node distance=10mm] 1430 \begin{tikzpicture}[baseline={([yshift=.5ex]s2)}] 1421 1431 \matrix [diag] (m) {% 1422 \node (s1) { }; & \node (t1) {};\\1423 \node (s2) { }; & \node (t2) {}; \\1432 \node (s1) {s_1}; & \node (t1) {s_1'};\\ 1433 \node (s2) {s_2}; & \node (t2) {s_2'}; \\ 1424 1434 }; 1425 1435 {[stealth] 1426 \draw (s1)  (t1);1427 \draw [new] (s2)  node [above] {$ *$} (t2);1436 \draw (s1)  node [above] {$\tau$} (t1); 1437 \draw [new] (s2)  node [above] {$\tau *$} (t2); 1428 1438 } 1429 1439 \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); 1430 \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S ,\L$} (t2);1440 \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); 1431 1441 \end{tikzpicture} 1432 \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} 1433 \label{subfig:cl_other_jump} 1434 \end{subfigure} 1435 & 1436 \begin{subfigure}{.375\linewidth} 1437 \centering 1438 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1439 every label/.style=overlay, node distance=10mm] 1440 \matrix [diag, small gap] (m) {% 1441 &\node (t1) {}; \\ 1442 \node (s1) [is call] {}; \\ 1443 && \node (l) {}; & \node (t2) {};\\ 1444 \node (s2) {}; & \node (c) [is call] {};\\ 1442 \qquad 1443 \begin{tikzpicture}[baseline={([yshift=.5ex]s2)}] 1444 \matrix [diag] (m) {% 1445 \node (s1) {s_1}; & \node (t1) {s_1'};\\ 1446 \node (s2) {s_2}; & \node (t2) {s_2'}; \\ 1447 }; 1448 {[stealth] 1449 \draw (s1)  node [above] {$L$} (t1); 1450 \draw [new] (s2)  node [above] {$L$} (t2); 1451 } 1452 \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); 1453 \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); 1454 \end{tikzpicture} 1455 \text{ if $L\notin\ell(\Functions)$} 1456 \qquad 1457 \begin{tikzpicture}[baseline={([yshift=.5ex]s2)}] 1458 \matrix [diag] (m) {% 1459 \node (s1) {s_1}; & \node (t1) {s_1'};\\ 1460 \node (s2) {s_2};\\ 1461 }; 1462 {[stealth] 1463 \draw (s1)  node [above] {$\ell(f)$} (t1); 1464 } 1465 \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); 1466 \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (s2); 1467 \end{tikzpicture} 1468 \\[10pt] 1469 \begin{tikzpicture} 1470 \matrix [diag, small vgap] (m) {% 1471 &\node (t1) {s_1'}; \\ 1472 \node (s1) {s_1}; \\ 1473 && \node (l1) {s_b}; & \node (l2) {s_c}; & \node (t2) {s_2'};\\ 1474 \node (s2) {s_2}; & \node (c) {s_a};\\ 1445 1475 }; 1446 1476 {[stealth] 1447 1477 \draw (s1)  node [above left] {$f$} (t1); 1448 \draw [new] (s2)  node [above] {$*$} (c); 1449 \draw [new] (c)  node [below right] {$f$} (l); 1450 \draw [new] (l)  node [above] {$*$} (t2); 1478 \draw [new] (s2)  node [above] {$\tau *$} (c); 1479 \draw [new] (c)  node [above left] {$f$} (l1); 1480 \draw [new] (l1)  node [above] {$\ell(f)$} (l2); 1481 \draw [new] (l2)  node [above] {$\tau *$} (t2); 1451 1482 } 1452 1483 \draw (s1) to [bend right] node [rel] {$\S$} (s2); 1453 1484 \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); 1454 \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);1455 1485 \draw [new] (t1) to [bend right] node [rel] {$\C$} (c); 1456 \end{tikzpicture} 1457 \caption{The \verb+cl_call+ case.} 1458 \label{subfig:cl_call} 1459 \end{subfigure} 1460 & 1461 \begin{subfigure}{.375\linewidth} 1462 \centering 1463 \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1464 every label/.style=overlay, node distance=10mm] 1465 \matrix [diag, small gap] (m) {% 1466 \node (s1) [is ret] {}; \\ 1467 &\node (t1) {}; \\ 1468 \node (s2) {}; & \node (c) [is ret] {};\\ 1469 && \node (r) {}; & \node (t2) {}; \\ 1486 \end{tikzpicture} 1487 \qquad\qquad 1488 \begin{tikzpicture} 1489 \matrix [diag, small vgap] (m) {% 1490 \node (s1) {s_1}; \\ 1491 &\node (t1) {s_1'}; \\ 1492 \node (s2) {s_2}; & \node (c) {s_a};\\ 1493 && \node (r) {s_b}; & \node (t2) {s_2'}; \\ 1470 1494 }; 1471 1495 {[stealth] 1472 1496 \draw (s1)  node [above right] {$RET$} (t1); 1473 \draw [new] (s2)  node [above] {$ *$} (c);1497 \draw [new] (s2)  node [above] {$\tau *$} (c); 1474 1498 \draw [new] (c)  node [below left] {$RET$} (r); 1475 \draw [new] (r)  node [above] {$ *$} (t2);1499 \draw [new] (r)  node [above] {$\tau *$} (t2); 1476 1500 } 1477 1501 \draw (s1) to [bend right] node [rel] {$\S$} (s2); 1478 \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S ,\L$} (t2);1502 \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S$} (t2); 1479 1503 \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); 1480 1504 \end{tikzpicture} 1481 \caption{The \verb+cl_return+ case.} 1482 \label{subfig:cl_return} 1483 \end{subfigure} 1484 \end{tabular} 1485 \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces. 1486 Dashed lines 1487 and arrows indicates how the diagrams must be closed when solid relations 1488 are present.} 1505 \caption{The hypotheses of ???. Dashed relations are implied by solid ones.} 1489 1506 \label{fig:forwardsim} 1490 1507 \end{figure} 1508 1509 1510 % \begin{figure} 1511 % \centering 1512 % \begin{tabular}{@{}c@{}c@{}c@{}} 1513 % % \begin{subfigure}{.475\linewidth} 1514 % % \centering 1515 % % \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1516 % % every label/.style=overlay, node distance=10mm] 1517 % % \matrix [diag] (m) {% 1518 % % \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ 1519 % % \node (s2) {}; & \node (t2) {}; \\ 1520 % % }; 1521 % % \node [above=0 of t1, overlay] {$\alpha$}; 1522 % % {[stealth] 1523 % % \draw (s1)  (t1); 1524 % % \draw [new] (s2)  node [above] {$*$} (t2); 1525 % % } 1526 % % \draw (s1) to node [rel] {$\S$} (s2); 1527 % % \draw [new] (t1) to node [rel] {$\S,\L$} (t2); 1528 % % \end{tikzpicture} 1529 % % \caption{The \verb+cl_jump+ case.} 1530 % % \label{subfig:cl_jump} 1531 % % \end{subfigure} 1532 % % & 1533 % \begin{subfigure}{.25\linewidth} 1534 % \centering 1535 % \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1536 % every label/.style=overlay, node distance=10mm] 1537 % \matrix [diag] (m) {% 1538 % \node (s1) {}; & \node (t1) {};\\ 1539 % \node (s2) {}; & \node (t2) {}; \\ 1540 % }; 1541 % {[stealth] 1542 % \draw (s1)  (t1); 1543 % \draw [new] (s2)  node [above] {$*$} (t2); 1544 % } 1545 % \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); 1546 % \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); 1547 % \end{tikzpicture} 1548 % \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} 1549 % \label{subfig:cl_other_jump} 1550 % \end{subfigure} 1551 % & 1552 % \begin{subfigure}{.375\linewidth} 1553 % \centering 1554 % \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1555 % every label/.style=overlay, node distance=10mm] 1556 % \matrix [diag, small gap] (m) {% 1557 % &\node (t1) {}; \\ 1558 % \node (s1) [is call] {}; \\ 1559 % && \node (l) {}; & \node (t2) {};\\ 1560 % \node (s2) {}; & \node (c) [is call] {};\\ 1561 % }; 1562 % {[stealth] 1563 % \draw (s1)  node [above left] {$f$} (t1); 1564 % \draw [new] (s2)  node [above] {$*$} (c); 1565 % \draw [new] (c)  node [below right] {$f$} (l); 1566 % \draw [new] (l)  node [above] {$*$} (t2); 1567 % } 1568 % \draw (s1) to [bend right] node [rel] {$\S$} (s2); 1569 % \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); 1570 % \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); 1571 % \draw [new] (t1) to [bend right] node [rel] {$\C$} (c); 1572 % \end{tikzpicture} 1573 % \caption{The \verb+cl_call+ case.} 1574 % \label{subfig:cl_call} 1575 % \end{subfigure} 1576 % & 1577 % \begin{subfigure}{.375\linewidth} 1578 % \centering 1579 % \begin{tikzpicture}[every join/.style={ar}, join all, thick, 1580 % every label/.style=overlay, node distance=10mm] 1581 % \matrix [diag, small gap] (m) {% 1582 % \node (s1) [is ret] {}; \\ 1583 % &\node (t1) {}; \\ 1584 % \node (s2) {}; & \node (c) [is ret] {};\\ 1585 % && \node (r) {}; & \node (t2) {}; \\ 1586 % }; 1587 % {[stealth] 1588 % \draw (s1)  node [above right] {$RET$} (t1); 1589 % \draw [new] (s2)  node [above] {$*$} (c); 1590 % \draw [new] (c)  node [below left] {$RET$} (r); 1591 % \draw [new] (r)  node [above] {$*$} (t2); 1592 % } 1593 % \draw (s1) to [bend right] node [rel] {$\S$} (s2); 1594 % \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); 1595 % \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); 1596 % \end{tikzpicture} 1597 % \caption{The \verb+cl_return+ case.} 1598 % \label{subfig:cl_return} 1599 % \end{subfigure} 1600 % \end{tabular} 1601 % \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces. 1602 % Dashed lines 1603 % and arrows indicates how the diagrams must be closed when solid relations 1604 % are present.} 1605 % \label{fig:forwardsim} 1606 % \end{figure} 1491 1607 1492 1608 \paragraph{1tomany forward simulation conditions.}
Note: See TracChangeset
for help on using the changeset viewer.