commit f87d4162349c404e8305c32bc7c7abf6f1b37461 Author: Zhengyi Chen Date: Fri Apr 19 03:04:18 2024 +0100 on L2 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e964244 --- /dev/null +++ b/.gitignore @@ -0,0 +1,301 @@ +## Core latex/pdflatex auxiliary files: +*.aux +*.lof +*.log +*.lot +*.fls +*.out +*.toc +*.fmt +*.fot +*.cb +*.cb2 +.*.lb + +## Intermediate documents: +*.dvi +*.xdv +*-converted-to.* +# these rules might exclude image files for figures etc. +# *.ps +# *.eps +# *.pdf + +## Generated if empty string is given at "Please type another file name for output:" +.pdf + +## Bibliography auxiliary files (bibtex/biblatex/biber): +*.bbl +*.bcf +*.blg +*-blx.aux +*-blx.bib +*.run.xml + +## Build tool auxiliary files: +*.fdb_latexmk +*.synctex +*.synctex(busy) +*.synctex.gz +*.synctex.gz(busy) +*.pdfsync + +## Build tool directories for auxiliary files +# latexrun +latex.out/ + +## Auxiliary and intermediate files from other packages: +# algorithms +*.alg +*.loa + +# achemso +acs-*.bib + +# amsthm +*.thm + +# beamer +*.nav +*.pre +*.snm +*.vrb + +# changes +*.soc + +# comment +*.cut + +# cprotect +*.cpt + +# elsarticle (documentclass of Elsevier journals) +*.spl + +# endnotes +*.ent + +# fixme +*.lox + +# feynmf/feynmp +*.mf +*.mp +*.t[1-9] +*.t[1-9][0-9] +*.tfm + +#(r)(e)ledmac/(r)(e)ledpar +*.end +*.?end +*.[1-9] +*.[1-9][0-9] +*.[1-9][0-9][0-9] +*.[1-9]R +*.[1-9][0-9]R +*.[1-9][0-9][0-9]R +*.eledsec[1-9] +*.eledsec[1-9]R +*.eledsec[1-9][0-9] +*.eledsec[1-9][0-9]R +*.eledsec[1-9][0-9][0-9] +*.eledsec[1-9][0-9][0-9]R + +# glossaries +*.acn +*.acr +*.glg +*.glo +*.gls +*.glsdefs +*.lzo +*.lzs +*.slg +*.slo +*.sls + +# uncomment this for glossaries-extra (will ignore makeindex's style files!) +# *.ist + +# gnuplot +*.gnuplot +*.table + +# gnuplottex +*-gnuplottex-* + +# gregoriotex +*.gaux +*.glog +*.gtex + +# htlatex +*.4ct +*.4tc +*.idv +*.lg +*.trc +*.xref + +# hyperref +*.brf + +# knitr +*-concordance.tex +# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files +# *.tikz +*-tikzDictionary + +# listings +*.lol + +# luatexja-ruby +*.ltjruby + +# makeidx +*.idx +*.ilg +*.ind + +# minitoc +*.maf +*.mlf +*.mlt +*.mtc[0-9]* +*.slf[0-9]* +*.slt[0-9]* +*.stc[0-9]* + +# minted +_minted* +*.pyg + +# morewrites +*.mw + +# newpax +*.newpax + +# nomencl +*.nlg +*.nlo +*.nls + +# pax +*.pax + +# pdfpcnotes +*.pdfpc + +# sagetex +*.sagetex.sage +*.sagetex.py +*.sagetex.scmd + +# scrwfile +*.wrt + +# svg +svg-inkscape/ + +# sympy +*.sout +*.sympy +sympy-plots-for-*.tex/ + +# pdfcomment +*.upa +*.upb + +# pythontex +*.pytxcode +pythontex-files-*/ + +# tcolorbox +*.listing + +# thmtools +*.loe + +# TikZ & PGF +*.dpth +*.md5 +*.auxlock + +# titletoc +*.ptc + +# todonotes +*.tdo + +# vhistory +*.hst +*.ver + +# easy-todo +*.lod + +# xcolor +*.xcp + +# xmpincl +*.xmpi + +# xindy +*.xdy + +# xypic precompiled matrices and outlines +*.xyc +*.xyd + +# endfloat +*.ttt +*.fff + +# Latexian +TSWLatexianTemp* + +## Editors: +# WinEdt +*.bak +*.sav + +# Texpad +.texpadtmp + +# LyX +*.lyx~ + +# Kile +*.backup + +# gummi +.*.swp + +# KBibTeX +*~[0-9]* + +# TeXnicCenter +*.tps + +# auto folder when using emacs and auctex +./auto/* +*.el + +# expex forward references with \gathertags +*-tags.tex + +# standalone packages +*.sta + +# Makeindex log files +*.lpz + +# xwatermark package +*.xwm + +# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib +# option is specified. Footnotes are the stored in a file with suffix Notes.bib. +# Uncomment the next line to have this generated file ignored. +#*Notes.bib diff --git a/.vscode/ltex.dictionary.en-US.txt b/.vscode/ltex.dictionary.en-US.txt new file mode 100644 index 0000000..1383873 --- /dev/null +++ b/.vscode/ltex.dictionary.en-US.txt @@ -0,0 +1,3 @@ +satisfiability +btwn +impl diff --git a/.vscode/ltex.hiddenFalsePositives.en-US.txt b/.vscode/ltex.hiddenFalsePositives.en-US.txt new file mode 100644 index 0000000..9f8fe46 --- /dev/null +++ b/.vscode/ltex.hiddenFalsePositives.en-US.txt @@ -0,0 +1,5 @@ +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qconcurrent components)\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qconcurrent components).\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qconcurrent components of a system).\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qprocess algebra).\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qalso holds for impl.\\E$"} diff --git a/01-spec-and-impl.pdf b/01-spec-and-impl.pdf new file mode 100644 index 0000000..369f6aa Binary files /dev/null and b/01-spec-and-impl.pdf differ diff --git a/01-spec-and-impl.tex b/01-spec-and-impl.tex new file mode 100644 index 0000000..57f70bd --- /dev/null +++ b/01-spec-and-impl.tex @@ -0,0 +1,248 @@ +\documentclass[99-notes-packed.tex]{subfiles} + +\begin{document} + +% \paragraph*{Specification vs. Implementation} +% \underbar{\textit{Specification}} describes what a system ought to satisfy and perform. \textbf{A \textit{formal specification}}, in particular, \textbf{is a specification derived using formal methods that ensure the required properties of some problem at hand}. A formal specification of a distributed system often comes in (at least) 2 parts: + +% \begin{enumerate} +% \item \textbf{ +% \textit{Requirements} imposed on the system -- i.e., a list of properties that the system should satisfy (e.g., safety / liveness properties). +% \label{def.spec.requirements} +% } +% \item \textbf{ +% \textit{Operations} of the system, which describes the behavior (i.e., satisfiability of predicates) given interactions (e.g., effects of communication). +% \label{def.spec.operations} +% } +% \end{enumerate} + +% In total, a formal specification is then used to verify the following: + +% \begin{enumerate} +% \item { +% Guarantee that a description of a system really meets the requirements of the same system -- i.e., the specification is correct. +% } +% \item \textbf{ +% Ensure that an \underbar{\textit{implementation}} satisfies the specification -- i.e., ensure that any correctness properties that hold for spec. also holds for impl. +% } +% \end{enumerate} + +\paragraph*{LTS and Process Graphs} +Both specifications and implementations could be represented by \underbar{\textit{models of concurrency}}, for example \textit{labelled transition systems (LTS)} or \textit{process graphs}. + +\begin{definition}[Process Graph] + A \textit{process graph} is a triple $(S, I, \rightarrowtriangle)$ such that: + \begin{itemize} + \item $S$ a set of states; + \item $I \in S$ an \textit{initial state}; + \item { + $\rightarrowtriangle$ a set of triples $(s, a, t)$ each describing a (named) relation $S \rightarrow S$: + \begin{itemize} + \item $s, t \in S$; + \item $a \in {Act}$ -- a set of actions. + \end{itemize} + } + \end{itemize} + \label{def.process-graph} +\end{definition} + +\begin{definition}[LTS] + Same as \hyperref[def.process-graph]{process graph}, except without an initial state. Sometimes used synonymously with process graphs bc. mathematicians are evil. +\end{definition} + +Alternatively, one may use \textit{process algebraic expressions} to formally represent spec.s and impl.s, for example using \textit{CCS (Calculus of Communicating Systems)}, \textit{CSP (Communicating Sequential Processes)}, and \textit{ACP (Algebra of Communicating Processes)}. \underline{Each semantics is of different expressive power}. + +\paragraph*{ACP} +Define the set of operations: +\begin{itemize} + \item { + $\varepsilon$ (successful termination -- $\mathrm{ACP}_{\varepsilon}$ extension). + } + \item { + $\delta$ (deadlock). + } + \item { + $a$ (action constant) for each action $a \in {Act}$. + + Each $a$ describe a \textbf{visible action} -- $\tau \notin {Act}$; + } + \item { + $P \cdot Q$ (sequential composition between processes $P, Q$) + } + \item { + $P + Q$ (summation / choice / alternative composition); + } + \item { + $P || Q$ (parallel composition). + } + \item { + ${\partial}_{H}(P)$ (restriction / encapsulation). + + Given set of (visible) actions $H$, this removes $\forall a \in H$ in $P$. + + Practically this is often used after defining $\gamma(a, b)$ to enforce sync -- via removing non-synced $a.b$ or $b.a$ behaviors; + } + \item { + ${\tau}_{I}(P)$ (abstraction -- $\mathrm{ACP}_{\tau}$ extension). + + Given set of (visible) actions $I$, this converts $\forall a \in I$ into $\tau$ in $P$. + + A $\tau$ action is \textbf{non-observable} -- this will be significant for describing traces \& equivalence relations. + } + \item { + $\gamma: A \times A \rightarrow A$ (partial communication function). + + For example, $\gamma(a, b)$ defines new (synchronized) visible action alongside $a, b$. + } +\end{itemize} + +We further define the following transition rules (omitting commutative equivalents). First, transition rules for basic process algebra wrt. termination, sequential composition, and choice: +\begin{center} + \begin{tabular}{ccc} + $ + \begin{prooftree} + \infer0{a \xrightarrow{a} \varepsilon} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} \varepsilon} + \infer1{a + b \xrightarrow{a} \varepsilon} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} \varepsilon} + \infer1{a \cdot b \xrightarrow{a} b} + \end{prooftree} + $ \\ + \\ + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} a^{'}} + \infer1{a + b \xrightarrow{a} a^{'}} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} a^{'}} + \infer1{a \cdot b \xrightarrow{a} a^{'} \cdot b} + \end{prooftree} + $ & + \\ + \end{tabular} +\end{center} + +Then, for parallel processes which may or may not communicate: +\begin{center} + \begin{tabular}{cc} + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} \varepsilon} + \infer1{a || b \xrightarrow{a} b} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} a^{'}} + \infer1{a || b \xrightarrow{a} a^{'} || b} + \end{prooftree} + $ \\ + \\ + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} \varepsilon} + \hypo{b \xrightarrow{b} \varepsilon} + \infer2{a || b \xrightarrow{\gamma(a, b)} \varepsilon} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} a^{'}} + \hypo{b \xrightarrow{b} \varepsilon} + \infer2{a || b \xrightarrow{\gamma(a, b)} a^{'}} + \end{prooftree} + $ \\ + \\ + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} \varepsilon} + \hypo{b \xrightarrow{b} b^{'}} + \infer2{a || b \xrightarrow{\gamma(a, b)} b^{'}} + \end{prooftree} + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{a} a^{'}} + \hypo{b \xrightarrow{b} b^{'}} + \infer2{a || b \xrightarrow{\gamma(a, b)} a^{'} || b^{'}} + \end{prooftree} + $ \\ + \end{tabular} +\end{center} + +Furthermore, for encapsulation ${\partial}_H$: +\begin{center} + \begin{tabular}{cc} + $ + \begin{prooftree} + \hypo{a \xrightarrow{x} \varepsilon} + \infer1{\partial_H(a) \xrightarrow{x} \varepsilon} + \end{prooftree}\ + x \notin H + $ & + $ + \begin{prooftree} + \hypo{a \xrightarrow{x} a^{'}} + \infer1{{\partial}_H(a) \xrightarrow{x} {\partial}_H(a^{'})} + \end{prooftree}\ + x \notin H + $ \\ + \end{tabular} +\end{center} +This is to say, $\partial_H(a)$ can execute all transitions of $a$ that are also not in $H$. + +Finally, deadlocks \textbf{does not display any behavior} -- that is, a $\delta$ process cannot transition to any other states no matter what (though obviously as a constituent part of e.g., a parallel process the other concurrent constituent can still run). + +\begin{background}[commutativity] + \begin{equation*} + f(a, b) = f(b, a) \iff f\ \mathrm{commutative} + \end{equation*} +\end{background} + +\begin{background}[associativity] + \begin{equation*} + (a \circ b) \circ c = a \circ (b \circ c) \iff \circ\ \mathrm{associative} + \end{equation*} +\end{background} + +\begin{background}[distributivity] + \begin{equation*} + f(x, a \circ b) = f(x, a) \circ f(x, b) \iff f\ \mathrm{distributes\ over}\ \circ + \end{equation*} +\end{background} + +\begin{background}[isomorphism] + An isomorphism describes a \textbf{bijective} \textbf{homomorphism}: + \begin{itemize} + \item { + \textbf{Homomorphism} describes a \textbf{structure-preserving} map between two algebraic \textbf{structures} of the same \textbf{type}: + \begin{itemize} + \item { + \textbf{Algebraic structure} describes a set with additional properties -- e.g., an additive group over $\mathbb{N}$, a ring of integers modulo $x$, etc. + } + \item { + Two structures of the same \textbf{type} refers to structures with the same name -- e.g., two groups, two rings, etc. + } + \item { + A \textbf{structure-preserving} map $f$ between two structures intuitively describes a structure such that, for properties $p \in X$, $q \in Y$ between same-type structures $X, Y$, any tuples $X^n \in p$ accepted by $p$ (e.g., $3 + 5 = 8 \implies (3, 5, 8) \in \mathbb{R}.(+)$) satisfies $\mathsf{map}(f, X^n) \in q$. + } + \end{itemize} + } + \item { + \textbf{Bijection} describes a 1-to-1 correspondence between elements of two sets -- i.e., invertible. + } + \end{itemize} +\end{background} + +\end{document} \ No newline at end of file diff --git a/02-semantic-equivalences.tex b/02-semantic-equivalences.tex new file mode 100644 index 0000000..e120769 --- /dev/null +++ b/02-semantic-equivalences.tex @@ -0,0 +1,27 @@ +\documentclass[99-notes-packed.tex]{subfiles} + +\begin{document} + +\begin{background}[lattice] + A \textbf{lattice} describes a real coordinate space $\mathbb{R}^n$ that satisfies: + \begin{itemize} + \item { + Addition / subtraction between two points always produce another point in lattice -- i.e., closed under addition / subtraction. + } + \item { + Lattice points are separated by bounded distances in some range $(0, \mathrm{max}]$. + } + \end{itemize} +\end{background} + +Define a lattice over which \textit{semantic equivalence relations} for spec. and impl. verification is defined. + +\begin{definition}[discrimination measure] + One equivalence relation $\equiv$ is \textbf{finer} / \textbf{more discriminating} than another $\sim$ if each $\equiv$-eq. class is a subset of a $\sim$-eq. class. In other words, + \begin{align*} + \ &p \equiv q \implies p \sim q \\ + \iff\ &\equiv\ \mathrm{finer\ than}\ \sim + \end{align*} +\end{definition} + +\end{document} \ No newline at end of file diff --git a/99-notes-packed.pdf b/99-notes-packed.pdf new file mode 100644 index 0000000..daba53e Binary files /dev/null and b/99-notes-packed.pdf differ diff --git a/99-notes-packed.tex b/99-notes-packed.tex new file mode 100644 index 0000000..7f92cab --- /dev/null +++ b/99-notes-packed.tex @@ -0,0 +1,39 @@ +\documentclass{article} + +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage[a4paper, margin=1cm]{geometry} + +\usepackage{multicol} % 2-col formatting +\usepackage{hyperref} +\usepackage[english]{babel} % theorem environ +\usepackage{framed} +\usepackage{mathtools} +\usepackage{stmaryrd} % more arrows +\usepackage{mathpartir} +\usepackage{graphicx} +\usepackage{tabularx} +\usepackage{ebproof} +\usepackage{amsmath} +\usepackage{amssymb} + +\usepackage{subfiles} % multi-file project + +% environment `definition` prints as "Definition" and has counter reset per section. +\newtheorem{definition}{Definition}[section] + +\newtheorem{background}{Background}[section] + +\begin{document} + +\section{LTS; ACP} +\begin{multicols*}{2} +\subfile{01-spec-and-impl} +\end{multicols*} + +\section{Semantic Equivalences} +\begin{multicols*}{2} +\subfile{02-semantic-equivalences} +\end{multicols*} + +\end{document} \ No newline at end of file