这是我第一次使用 latex，我使用的是提供给我的模板文件。
以下代码（部分）在子部分之前生成了一个空白页。
\documentclass[10pt]{article}
\usepackage[urlcolor=blue,colorlinks=true,pdfstartview=FitH,bookmarks=false]{hyperref}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{alltt}
\usepackage{amsfonts}
\usepackage{semantic}
\usepackage{listings}
\usepackage{multirow}
\newcommand{\lsyn}{|[} % A macro for left semantic brackets.
\newcommand{\rsyn}{|]} % A macro for right semantic brackets.
\newcommand{\COMMENT}[1]{}
%\newcommand{\TODO}[1]{\textbf{[TODO: #1]}\\}
\newcommand{\TODO}[1]{}
\newcommand{\DONE}[1]{}
\newcommand{\CBD}[1]{}
\newcommand{\ignore}[1]{}
\newcommand{\ALT}{$|$}
\newcommand{\figref}[1]{Fig.~\ref{Fi:#1}}
\newcommand{\TRUE}{\texttt{tt}}
\newcommand{\FALSE}{\texttt{ff}}
\newcommand{\While}{\textbf{While}}
\newcommand{\If}{\textbf{if}}
\newcommand{\Then}{\textbf{then}}
\newcommand{\Else}{\textbf{else}}
\newcommand{\Do}{\textbf{do}}
\newcommand{\Skip}{\texttt{skip}}
\newcommand{\FVar}{\textit{FV}}
\newcommand{\Var}{\textit{Var}}
\newcommand{\Abort}{\texttt{abort}}
\newcommand{\Assume}{\texttt{assume}}
\newcommand{\Or}{\texttt{or}}
\newcommand{\Begin}{\texttt{begin}}
\newcommand{\End}{\texttt{end}}
\newcommand{\Par}{\texttt{par}}
\newcommand{\Fib}{\textit{Fib}}
\newcommand{\Int}{\mathbb{Z}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Num}{\textbf{Num}}
\newcommand{\TrueVal}{\textbf{tt}}
\newcommand{\FalseVal}{\textbf{ff}}
\newcommand{\Bool}{\{\TrueVal, \FalseVal\}}
\newcommand{\Aexp}{\textbf{Aexp}}
\newcommand{\Bexp}{\textbf{Bexp}}
\newcommand{\State}{\textbf{State}}
\newcommand{\derives}{\rightarrow}
\newcommand{\Stm}{\textrm{Stm}}
\newcommand{\Asem}{\mathcal{A}}
\newcommand{\Bsem}{\mathcal{B}}
\newcommand{\Ssem}{\mathcal{S}}
\newcommand{\Hash}{\texttt{hash}}
\newcommand{\GCD}{\texttt{gcd}}
\newcommand{\Val}[2]{{#1}{\mapsto}{#2}}
\begin{document}
\title{Program Analysis and Verification\\Homework Assignment \#1}
\author{Students: Yoav Cohen, ID: 201053287, [email protected]\\and Yinon Eliraz, ID: 305335911, [email protected]}
\date{\today}
\maketitle
\begin{abstract}
This file is intended to help you get started with \LaTeX\ by showing examples
of typesetting mathematical notations for assignment 1.
You should erase any text that is not needed by your solution (like this abstract)
and add your own answer.
\end{abstract}
% Here are a few helpful macros
\newcommand{\While}{\textbf{While}}
\newcommand{\Int}{\mathbb{Z}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Num}{\textbf{Num}}
\newcommand{\Bool}{\{\TrueVal, \FalseVal\}}
\newcommand{\Aexp}{\textbf{Aexp}}
\newcommand{\Bexp}{\textbf{Bexp}}
\newcommand{\State}{\textbf{State}}
\newcommand{\derives}{\rightarrow}
\newcommand{\Var}{\textit{Var}}
\newcommand{\FV}{\textit{FV}}
\newcommand{\Stm}{\textrm{Stm}}
\newcommand{\Asem}{\mathcal{A}}
\newcommand{\Bsem}{\mathcal{B}}
\newcommand{\Abort}{\texttt{abort}}
\newcommand{\Assume}{\texttt{assume}}
\newcommand{\Or}{\texttt{or}}
\newcommand{\Begin}{\texttt{begin}}
\newcommand{\End}{\texttt{end}}
\newcommand{\Par}{\,\texttt{par}\,}
\newcommand{\Hash}{\texttt{hash}}
\newcommand{\GCD}{\texttt{gcd}}
\newcommand{\Val}[2]{{#1}{\mapsto}{#2}}
\section{Warm-up \small{(38pt})}
\paragraph{(a) Evaluating the Program.}
\begin{small}
\[
\begin{array}{rl}
& \langle \Hash, [\Val{t}{-1}, \Val{a}{-1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ t=0;a=1;W;r=a, [\Val{t}{-1}, \Val{a}{-1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ a=1;W;r=a, [\Val{t}{0}, \Val{a}{-1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ W;r=a, [\Val{t}{0}, \Val{a}{1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ t=t+1;a=a*31+t;W;r=a, [\Val{t}{0}, \Val{a}{1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ a=a*31+t,W;r=a, [\Val{t}{1}, \Val{a}{1}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ W;r=a, [\Val{t}{1}, \Val{a}{32}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ t=t+1;a=a*31+t;W;r=a, [\Val{t}{1}, \Val{a}{32}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ a=a*31+t;W;r=a, [\Val{t}{2}, \Val{a}{32}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ W;r=a, [\Val{t}{2}, \Val{a}{994}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ t=t+1;a=a*31+t;W;r=a, [\Val{t}{2}, \Val{a}{994}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ a=a*31+t;W;r=a, [\Val{t}{3}, \Val{a}{994}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ W;r=a, [\Val{t}{3}, \Val{a}{30817}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \langle \ r=a, [\Val{t}{3}, \Val{a}{30817}, \Val{r}{-1}, \Val{x}{3}] \rangle\\
\derives & \ [\Val{t}{3}, \Val{a}{30817}, \Val{r}{30817}, \Val{x}{3}] \\
\end{array}
\]
\end{small}
\newpage
\subsection{Termination Precondition \small{(17pt})}
The set $P$ is the following:
\[
P = \{ \sigma \;|\; \sigma = [\Val{a}{x}, \Val{b}{x}] \} \cup \{ \sigma \;|\; \sigma = [\Val{a}{n_1}, \Val{b}{n_2}] \wedge n_1>0 \wedge n_2>0 \wedge n_1 \neq n_2 \}
\] \\
\noindent
\textbf{First Part:} will prove correctness for $\sigma = [\Val{a}{x}, \Val{b}{x}]$ :
\noindent
\begin{small}
\noindent
\[
\begin{array}{rl}
& \langle \GCD, [\Val{a}{x}, \Val{b}{x}] \rangle\\
\derives & \langle \ W, [\Val{a}{x}, \Val{b}{x}] \rangle\\
\derives & \ [\Val{a}{x}, \Val{b}{x}] \\
\end{array}
\]
\end{small}
\noindent
\textbf{Second Part:} will prove correctness for $\sigma = [\Val{a}{n_1}, \Val{b}{n_2}] \wedge n_1>0 \wedge n_2>0 \wedge n_1 \neq n_2$ : \\
Let $\sigma_i$ be the state after i iterations of while meaning:
\newline
\langle \text{W} , $\sigma$\rangle \overset {2*i} \rightarrow\langle \text{W} , $\sigma_i$\rangle \\
$ And let $s_i$ be the new the sum of a and b after i iterations mening:
\newline
$s_i$ = $\sigma_i$a + $\sigma_i$b
\newline
\underline{Distinction:}\ If $\sigma = [\Val{a}{n_1}, \Val{b}{n_2}] \wedge n_1>0 \wedge n_2>0 \wedge n_1 \neq n_2$ then $s_0$ $>$ 0
\newline
\underline{Auxiliary argument:} If \langle \text{W} , $\sigma_i$\rangle \overset {2} \rightarrow\langle \text{W} , $\sigma_j$ \rangle \, \wedge \, $\sigma_i$a $>$ 0 \, \wedge \, $\sigma_i$b $>$ 0 then $s_i > s_j$ and $s_j > 0 $
\newline
\underline{Proof:} There are 2 cases:
\newline
First case , $\sigma_i$a $>$ $\sigma_i$b:
\neline
\begin{small}
\noindent
\[
\begin{array}{rl}
& \langle \ W, s_i = [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ if.., [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ W, s_j = [\Val{a}{n_1 - n_2}, \Val{b}{n_2}] \rangle\\
\end{array}
\]
\end{small}
but $n_1>n_2$ and $n_1 , n_2 >0$ so it is easy to see that $s_i > s_j$ and $s_j > 0 $
\newline
\newline
Second case , $\sigma_i$b $>$ $\sigma_i$a:
\neline
\begin{small}
\noindent
\[
\begin{array}{rl}
& \langle \ W, s_i = [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ if.., [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ W, s_j = [\Val{a}{n_1}, \Val{b}{n_2 - n_1}] \rangle\\
\end{array}
\]
\end{small}
but $n_1<n_2$ and $n_1 , n_2 >0$ so it is easy to see that $s_i > s_j$ and $s_j > 0 $
\underline{Conclusion:} If $\sigma_i$a $>$ 0 \, \wedge \, $\sigma_i$b $>$ 0 and \langle \text{W} , $\sigma_i$\rangle \overset {2*i} \rightarrow\langle \text{W} , $\sigma_k$\rangle \ then \, $s_i > s_{i+1} > s_{i+2} ...> s_{k}$ \\
ֿֿ\newline
\underline{Main Proof:} Now by using the Distinction, Auxiliary argument and the Conclusion we can infer that S is getting
lower in each iteration but it will never be zero, In addition we are dealing with natural numbers only so eventually the
loop will have to terminate.
Q.E.D
\newline
\newline
\textbf{Third Part:} Now we will explain non-termination for any other states : \\
The only left stats are $\sigma = [\Val{a}{n_1}, \Val{b}{n_2}] \wedge ( $0\geq n_1$ \, \vee \, $0\geq n_2$ \wedge n_1 \neq n_2$ ) : \\
\newline
Without loss of generality $n_1 > n_2 $ :
\neline
\begin{small}
\noindent
\[
\begin{array}{rl}
& \langle \ W, [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ if.., [\Val{a}{n_1}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ W, [\Val{a}{n_1 - n_2}, \Val{b}{n_2}] \rangle\\
\end{array}
\]
\end{small}
but $n_1>n_2$ so $0\geq n_2$ what makes $n_1 - n_2 \geq n_1 > n_2 $ what will make a and b never be even so will enter infinite loop:
\neline
\begin{small}
\noindent
\[
\begin{array}{rl}
& \langle \ W, [\Val{a}{n_1 - n_2}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ if.., [\Val{a}{n_1 - n_2}, \Val{b}{n_2}] \rangle\\
\derives & \langle \ W, [\Val{a}{(n_1 - n_2)-n_2}, \Val{b}{n_2}] \rangle\\
...
\end{array}
\]
\end{small}
Q.E.D
\section{Semantic Equivalence \small{(30pt})}
\subsection{Equivalence 1 \small{(5pt})}
Two cases: \\
1. $\Bsem \lsyn b \rsyn$= tt: \\
\langle \text{if b then skip else abort} , $\sigma$ \rangle \rightarrow \langle skip , $\sigma$ \rangle \rightarrow $\sigma$\\
\langle \text{assume b} , $\sigma$\rangle \rightarrow $\sigma$\\
\text{So in this case on successfully terminating derivations we got equivalence.} \\
2. $\Bsem \lsyn b \rsyn$= ff: \\
\langle \text{if b then skip else abort} , $\sigma$ \rangle \rightarrow \langle abort , $\sigma$ \rangle \rightarrow \text{undefined}\\
\langle \text{assume b} , $\sigma$\rangle \rightarrow undefined \\
\text{So in this case on successfully terminating derivations we got equivalence.} \\
\text {Q.E.D} \\
\subsection{Equivalence 2 \small{(10pt})}
Two cases: \\
1. $\Bsem \lsyn b \rsyn$= tt: \\
\langle \text{if b then $S_1$ else $S_2$} , $\sigma$ \rangle \rightarrow \langle $S_1$ , $\sigma$ \rangle \\
\langle \text{(assume b; $S_1$) or (assume \neg b; $S_2$)} , $\sigma$ \rangle \rightarrow \langle \text{assume b; $S_1$} , $\sigma$ \rangle \rightarrow \langle \text{$S_1$} , $\sigma$ \rangle \\
\langle \text{(assume b; $S_1$) or (assume \neg b; $S_2$)} , $\sigma$ \rangle \rightarrow \langle \text{assume \neg b; $S_2$} , $\sigma$ \rangle \rightarrow undefined \\ \\
\text{So in this case on successfully terminating derivations we got equivalence.} \\
2. $\Bsem \lsyn b \rsyn$= ff :\\
\langle \text{if b then $S_1$ else $S_2$} , $\sigma$ \rangle \rightarrow \langle $S_2$ , $\sigma$ \rangle \\
\langle \text{(assume b; $S_1$) or (assume \neg b; $S_2$)} , $\sigma$ \rangle \rightarrow \langle \text{assume b; $S_1$} , $\sigma$ \rangle \rightarrow undefined \\
\langle \text{(assume b; $S_1$) or (assume \neg b; $S_2$)} , $\sigma$ \rangle \rightarrow \langle \text{assume \neg b; $S_2$} , $\sigma$ \rangle \rightarrow \langle \text{$S_2$} , $\sigma$ \rangle \\
\text{So in this case on successfully terminating derivations we got equivalence.} \\
\text {Q.E.D} \\
\subsection{Equivalence 3 \small{(15pt})}
We prove that if $\langle S_1, \sigma\rangle \derives^{k} \sigma'$
and $\langle S_2, \sigma'\rangle \derives^{m} \sigma''$ then
$\langle S_1; S_2\rangle \derives^{k+m} \sigma''$ by proving the following lemma with induction on k:
\begin{theorem*}
if $\langle S_1, \sigma\rangle \derives^{k} \sigma'$ then
$\langle S_1; S_2, \sigma \rangle \derives^{k} \langle S_2, \sigma' \rangle$. \\
\end{theorem*}
\paragraph{Base case.} $k=1$\\
\text{Then:}\\
\text{1. } $\langle S_{1}, \sigma \rangle \rightarrow \sigma ' $\\
\text{By operating derivation rules we get: } \\
$ \langle S_{1};S_{2}, \sigma \rangle \underset{\text{comp2}}{\rightarrow} \langle S_2, \sigma' \rangle$ Q.E.D \\
\paragraph{Induction Hypothesis.}
\text{Assuming the lemma for k=n-1 }
\paragraph{Induction Step.}
\text{Under the induction hypothesis we will prove for k=n}\\
Let $k=n$ and suppose that $\langle S_1, \sigma\rangle \derives^{n} \sigma'$. We will show that $\langle S_1; S_2, \sigma \rangle \derives^{n} \langle S_2, \sigma' \rangle$. \\
proof: n$>$1 so we can infer that there is configuration such that: \\
\[\langle S_1, \sigma\rangle \derives^{1} \langle S_1',\sigma_1' \rangle \derives^{n-1} \sigma' \]
Now we can apply the induction on $\langle S_1', \sigma_1' \rangle \derives^{n-1} \sigma' $ so we will get:\\
\[\langle S_1';S_2 ,\sigma_1' \rangle \derives^{n-1} \langle S_2 ,\sigma' \rangle \] \\
So overall we got:
\[\langle S_1;S_2 ,\sigma \rangle \underset{\text{comp1}}\derives \langle S_1';S_2 ,\sigma_1' \rangle \derives^{n-1} \langle S_2 ,\sigma' \rangle \] \\
so the lemma holds for n$=$k.
\paragraph{Main Proof.}
\text Assume that (1) $\langle S_1, \sigma\rangle \derives^{k} \sigma'$
and (2) $\langle S_2, \sigma'\rangle \derives^{m} \sigma''$ \\
So from the lemma and the above: \\
\[ \langle S_1; S_2, \sigma\rangle \underset{\text{lemma and (1)}} \derives^{k} \langle S_2 ,\sigma' \rangle \underset{\text{(2)}} \derives^{m} \sigma'' \] Q.E.D \\
\clearpage
\section{Parallelism with Transactional Semantics \small{(30pt})}
\subsection{Configurations \small{(10pt})}
We define parallel configurations as follows:
We will use both the \emph{sequential configurations} $\langle S,\sigma\rangle$ and $\sigma$
and add two more types of configurations.
Let $R,R_1,R_2$ and $W,W_1,W_2$ denote sets of variables read so far,
written to so far, respectively.
%
Let $\delta, \delta_1, \delta_2$ denote partial states, used for
backing up values of variables.
\emph{Local configurations} have the form
$\langle S, \sigma, R, W, \delta \rangle$ and $\langle \sigma, R, W, \delta \rangle$,
where $R, W \subseteq \Var$ and $\delta \in W \rightarrow \Int$ $(\delta(v)=z$, such that z is the last value in $\sigma$, before entering a parallel expression).
\emph{Global configurations} have the form
\[
\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \enspace.
\]
\newcommand{\Conflict}{\textit{conflict}}
\newcommand{\Rollback}{\textit{rollback}}
We will also define the predicate $\Conflict : 2^{Var} \times 2^{Var} \times 2^{Var} \times 2^{Var} \rightarrow \{\TRUE,\FALSE\}$ and $\Rollback : (\State \times \State) \rightarrow \State$ such that:
\[
\Conflict (R_1,R_2,W_1,W_2) =
\begin{cases}
\TRUE, & \begin{array}{@{}lr@{}}
W_1 \cap W_2 \neq \emptyset \,\vee\\
W_1 \cap R_2 \neq \emptyset \,\vee\\
W_2 \cap R_1 \neq \emptyset\\
\end{array}\\
\FALSE, & \text{else}\\
\end{cases}
\]
\Rollback(\sigma, \delta) = \{\,<x,z> \in \sigma \mid x \notin dom(\delta) \,\} \cup \delta \\
We used the Early Conflict Detection Policy.
The conflict predicate will check each iteration of global confirmation if a data conflict as occurred. \\
If there was a conflict we will use the Rollback function to revert all the actions of one of the statements(S1 or S2).
\subsection{Rules 1 \small{(5pt})}
We define the following rules
the if statements are correlated for the upper definition (there wasn't enough space in the line)
\[
\begin{array}{ll}
\textbf{[par]} &
\langle (\Begin \ 1; S_1; \End \ 1) \ \Par \ (\Begin \ 2; S_2; \End \ 1), \sigma \rangle \derives \\ & \langle (\Begin \ 1; S_1; \End \ 1) \ \Par \ , \emptyset, \emptyset, \emptyset,(\Begin \ 2; S_2; \End \ 1) ,\emptyset, \emptyset, \emptyset, \sigma \rangle \\ \\
\textbf{[begin1-L]} & \langle\Begin \ 1, \sigma, R, W, \delta \rangle\derives \langle \sigma, R, W, \delta \rangle \ \ \\ \\
\textbf{[begin2-L]} & \langle\Begin \ 2, \sigma, R, W, \delta \rangle\derives \langle \sigma, R, W, \delta \rangle \ \ \\ \\
\textbf{[end1-L]} & \langle \End \ 1, \sigma, R, W, \delta \rangle \derives \langle \sigma, R, W, \delta \rangle \ \ \\ \\
\textbf{[end2-L]} & \langle \End \ 2, \sigma, R, W, \delta \rangle \derives \langle \sigma, R, W, \delta \rangle \ \ \\ \\
\textbf{[begin1]} & \langle\Begin \ 1, \sigma \rangle \derives \sigma \ \ \\ \\
\textbf{[begin2]} & \langle\Begin \ 2, \sigma \rangle \derives \sigma \ \ \\ \\
\textbf{[end1]} & \langle \End \ 1, \sigma \rangle \derives \sigma \ \ \\ \\
\textbf{[end2]} & \langle \End \ 2, \sigma \rangle \derives \sigma \ \ \\ \\
\textbf{[par-t$^1$]} &
\inference{\langle S_1,\sigma, R_1, W_1, \delta_1 \rangle \derives \langle \sigma', R_1', W_1', \delta_1' \rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_2, \sigma' \rangle} \\ \\
\textbf{[par-c$^1$]} &
\inference{\langle S_1,\sigma, R_1, W_1, \delta_1 \rangle \derives \langle S_1',\sigma', R_1', W_1', \delta'_1\rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_1', R_1', W_1', \delta_1', S_2, R_2, W_2, \delta_2, \sigma' \rangle } \\ \\ & \textbf{ if } \Conflict (R_1', R_2, W_1', W_2) = \FALSE \\ \\
\textbf{[par-r$^1$]} &
\inference{\langle S_1,\sigma, R_1, W_1, \delta_1 \rangle \derives \langle S_1',\sigma', R_1', W_1', \delta'_1\rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_2, \Rollback(\delta_1, \sigma) \rangle } \\ \\ & \textbf{ if } \Conflict (R_1', R_2, W_1', W_2) = \TRUE \\ \\
\textbf{[par-t$^2$]} &
\inference{\langle S_2,\sigma, R_2, W_2, \delta_2 \rangle \derives \langle \sigma', R_2', W_2', \delta_2' \rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_1, \sigma' \rangle} \\ \\
\textbf{[par-c$^2$]} &
\inference{\langle S_2,\sigma, R_2, W_2, \delta_2 \rangle \derives \langle S_2',\sigma', R_2', W_2', \delta'_2\rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_1, R_1, W_1, \delta_1, S_2', R_2', W_2', \delta_2', \sigma' \rangle } \\ \\ & \textbf{ if } \Conflict (R_1, R_2', W_1, W_2') = \FALSE \\ \\
\textbf{[par-r$^2$]} &
\inference{\langle S_2,\sigma, R_2, W_2, \delta_2 \rangle \derives \langle S_2',\sigma', R_2', W_2', \delta'_2\rangle}{\langle S_1, R_1, W_1, \delta_1, S_2, R_2, W_2, \delta_2, \sigma \rangle \derives \langle S_1, \Rollback(\delta_2, \sigma) \rangle} \\ \\ & \textbf{ if } \Conflict (R_1, R_2', W_1, W_2') = \TRUE \\ \\
\\
\end{array}
\]
We used $[par]$ when we want to move from normal configuration to global run in order to run the 2 tasks. \\
$[par-t]$ is a rule to handle a states when one of the tasks finished without a conflict and now only the second task should run. \\
$[par-c]$ is a rule to commit a task change when no conflict has occurred. \\
$[par-r]$ is a rule to revert all task changes when a conflict has occurred. \\
\subsection{Rules 2 \small{(5pt})}
\text{} \\ \\
\[
\begin{array}{ll}
\textbf{[skip-L]} &
\langle \Skip, \sigma, R, W, \delta \rangle \derives \langle \sigma, R, W, \delta \rangle \\ \\
\textbf{[comp-L$^1$]} &
\inference{\langle S_1, \sigma, R, W, \delta \rangle \derives \langle S_1',\sigma', R', W', \delta'\rangle}{\langle S_1;S_2,\sigma, R, W, \delta \rangle \derives \langle S'_1;S_2,\sigma', R', W', \delta' \rangle} \\ \\
\textbf{[comp-L$^2$]} &
\inference{\langle S_1, \sigma, R, W, \delta \rangle \derives \langle \sigma', R', W', \delta'\rangle}{\langle S_1;S_2,\sigma, R, W, \delta \rangle \derives \langle S_2,\sigma', R', W', \delta' \rangle} \\ \\
\textbf{[ass-L]} &
\langle x := a, \sigma, R, W, \delta \rangle \derives \langle \sigma [\Val{x}{\Asem \lsyn a \rsyn \sigma}], R\cup FV(a), W\cup\{x\}, \textit{backup}(\delta, x , \sigma \lsyn x \rsyn \rangle \\ \\
\textbf{[if-L$^{\textbf{ff}}$]} &
\langle \text{If $b$ then $S_1$ else $S_2$}, \sigma, R, W, \delta \rangle \derives \langle S_2, \sigma, R\cup FV(b), W, \delta \rangle \ \ \ \text{if} \ \Bsem \lsyn b \rsyn \sigma = \FALSE \\ \\
\textbf{[if-L$^{\textbf{tt}}$]} &
\langle \text{If $b$ then $S_1$ else $S_2$}, \sigma, R, W, \delta \rangle \derives \langle S_1, \sigma, R\cup FV(b), W, \delta \rangle \ \ \ \text{if} \ \Bsem \lsyn b \rsyn \sigma = \TRUE \\ \\
\textbf{[while-L$^{\textbf{tt}}$]} &
\langle \text{while $b$ do $S$}, \sigma, R, W, \delta \rangle \derives \langle S;\text{While $b$ do $S$}, \sigma, R \cup FV(b), W, \delta \rangle \ \ \ \text{if} \ \Bsem \lsyn b \rsyn \sigma = \TRUE \\ \\
\textbf{[while-L$^{\textbf{ff}}$]} &
\langle \text{while $b$ do $S$}, \sigma, R, W, \delta \rangle \derives \langle \sigma, R \cup FV(b), W, \delta \rangle \ \ \ \text{if} \ \Bsem \lsyn b \rsyn \sigma = \FALSE \\ \\
\\
\end{array}
\]
Backup function is using in order to backup the value of variable before its first assignment within a task.
$\backup : (\State \times V \times Z ) \rightarrow \State$ such that:
\[
\textit{backup}(\delta, v, n) =
\begin{cases}
\delta \cup \langle v,n \rangle, & \ v \notin \text{Dom}(\delta)\\
\delta, & \text{else}\\
\end{cases}
\]
\noindent
No other major Changes expect from the fact we had to update the read/write sets according to each rule.
\newpage
\subsection{Exemplify \small{(10pt})}
\subsubsection{Race free execution}
Here, we assume that the state $ \sigma $ holds $ \sigma = \{c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0\}$ \\ \\
$\langle$ (begin 1 ; if b=1 then a:=a+1 else f :=b+c ; end 1 )
par
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 )
, $ [c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$ (begin 1 ; if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 2, b \rightarrow 1 , a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$ (if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$ (if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
(if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$ ( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
($g:=b \cdot c$; end 2 ),$\{ c\},\emptyset,\emptyset$
, $ [c \rightarrow 2, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow ] \rangle \derives$ \\ \\
$\langle$ ( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
(end 2 ),$\{ c, a, b\},\{ g \}, [g \rightarrow 0 ] $
, $ [c \rightarrow 2, b \rightarrow 1, g \rightarrow 2, f \rightarrow 0 ] \rangle \derives$ \\ \\
$\langle$ ( end 1 )
,$\{ b \},\{a\},[ a \rightarrow 0],$
(end 2 ),$\{ c, a, b\},\{ g \}, [g \rightarrow 0 ] $
, $ [c \rightarrow 2, b \rightarrow 1, g \rightarrow 2, a \rightarrow 1, f \rightarrow 0] \rangle \derives$ \\ \\
$\langle$
(end 2 ),$ [c \rightarrow 2, b \rightarrow 1, g \rightarrow 2, a \rightarrow 1, f \rightarrow 0] \rangle \derives$ \\ \\
$ [c \rightarrow 2, b \rightarrow 1, g \rightarrow 2, a \rightarrow 1, f \rightarrow 0]$
\subsubsection{Aborting execution}
Here, we assume that the state $ \sigma $ holds $ \sigma = \{c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0\}$ \newline\newline
$\langle$ (begin 1 ; if b=1 then a:=a+1 else f :=b+c ; end 1 )
par
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 )
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$ (begin 1 ; if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 1, b \rightarrow 1 , a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$ (if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(begin 2 ; if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$ (if b=1 then a:=a+1 else f :=b+c ; end 1 )
,$\emptyset,\emptyset,\emptyset,$
(if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
(if c=1 then a:=a+2 else $g:=b \cdot c$ ; end 2 ),$\emptyset,\emptyset,\emptyset$
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$ ( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
(a:=a+2; end 2 ),$\{ c\},\emptyset,\emptyset$
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 0, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$\langle$ ( a:=a+1; end 1 )
,$\{ b \},\emptyset,\emptyset,$
(end 2 ),$\{ c, a\},\{a \}, [a \rightarrow 0] $
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 2, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\
\[
\text{conflict, rollback S1}
\]\\
$\langle$
(end 2 )
, $ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 2, f \rightarrow 0 , g \rightarrow 0] \rangle \derives$ \\ \\
$ [c \rightarrow 1, b \rightarrow 1, a \rightarrow 2, f \rightarrow 0 , g \rightarrow 0]$
\newpage
\section*{Questionnaire (optional)}
Please provide feedback for this assignment:
\begin{enumerate}
\item \textbf{Q:} Was this assignment useful for understanding the material?
\textbf{A:} Yes it was really helpfull to try it by ourself.
\item \textbf{Q:} How much time did you spend on this assignment?
\textbf{A:} Part 3 was too complicated in my opinion comparing to any assignment we had.
The Tips you gave were very helpfull but there so many small nuances in the question
and we never did something similair in class what makes us stop counting how much time
we spent on finding the proper solution for this question
\item \textbf{Q:} How hard would you say this assignment was: trivial/easy/okay/hard/very challenging?
\textbf{A:} hard.
\item \textbf{Q:} Any comments/suggestions for the course so far?
\textbf{A:} Well...
\end{enumerate}
\end{document}
当我删除时，\subsection空白页消失了。
我不知道为什么会发生这种情况。有什么想法吗？