figs-only.tex

\documentclass{article}

\usepackage{amsmath}

\newcommand{\Prog}{p}
\newcommand{\Progy}{p'}
\newcommand{\Reg}{x}
\newcommand{\Word}{w}
\newcommand{\Val}{v}
\newcommand{\Valy}{v'}
\newcommand{\Stack}{t}
\newcommand{\Heap}{h}
\newcommand{\Undef}{\mathtt{undef}}
\newcommand{\CodeFrag}{CF}
\newcommand{\HeapMap}{H}
\newcommand{\HeapMapy}{H'}
\newcommand{\TaskMap}{T}
\newcommand{\TaskMapy}{T'}
\newcommand{\Task}{s}
\newcommand{\Tasky}{s'}
\newcommand{\TName}{t}
\newcommand{\TNamey}{t'}
\newcommand{\FName}{f}
\newcommand{\HName}{h}
\newcommand{\Env}{c}
\newcommand{\Envy}{c'}
\newcommand{\State}{S}
\newcommand{\Code}{L}
\newcommand{\Codey}{L'}
\newcommand{\Local}{\sigma}

\newcommand{\reduces}[1][]{\xrightarrow{{#1}}}
\newcommand{\Reduces}{\rightarrow}
\newcommand{\EReduces}[2][\TName]{\reduces[{\OP[{#1}]{#2}}]}
\newcommand{\IReduces}[2][\TName]{\reduces[{\OP[{#1}]{#2}}]}
\newcommand{\PReduces}[2][\TName]{\reduces[{\OP[{#1}]{#2}}]}
\newcommand{\SReduces}[1]{\reduces[#1]}
\newcommand{\Put}[2]{\{{#1}:={#2}\}}

\newcommand{\putGlobal}[3]{\mathrm{putGlobal}({#1},{#2},{#3})}
\newcommand{\putLocal}[4]{\mathrm{putLocal}({#1},{#2},{#3},{#4})}
\newcommand{\spawn}[4]{\mathrm{spawn}({#1},{#2},{#3},{#4})}
\newcommand{\EEval}[2]{\mathrm{eval}{({#1},{#2})}}
\newcommand{\setProg}[3]{\mathrm{setProg}{({#1},{#2},{#3})}}

\newcommand{\Inst}{i}
\newcommand{\Nil}{\mathtt{nil}}
\newcommand{\Args}{A}
\newcommand{\Op}{o}
\newcommand{\Var}{x}
\newcommand{\Exp}{e}
\newcommand{\Deref}[1][\Val]{*{#1}}
\newcommand{\Store}[1][\Val]{\Deref[{#1}] = }
\newcommand{\Nat}{z}
\newcommand{\Naty}{z'}
\newcommand{\Malloc}{\mathtt{malloc}}
\newcommand{\Future}[3]{\mathtt{future}\ {#1}\ {#2}.{#3}}
\newcommand{\Force}[1][\Val]{\mathtt{force}\ {#1}}
\newcommand{\If}[3][\Val]{\mathtt{if}\ {#1}\ {#2}\ {#3}}
\newcommand{\Ret}[1][\Val]{\mathtt{ret}\ {#1}}
\newcommand{\TStatus}{b}
\newcommand{\HeapVal}{u}
\newcommand{\Node}{n}
\newcommand{\Edges}{E}
\newcommand{\Access}{a}
\newcommand{\Edge}{e}
\newcommand{\Nodes}{l}
\newcommand{\AccessMap}{A}
\newcommand{\Time}{N}
\newcommand{\CG}{C}

\newcommand{\GetLocal}[3][\State]{\mathrm{local}({#1},{#2},{#3})}
\newcommand{\Program}[3][\State]{{\mathrm{prog}({#1},{#2},{#3})}}
\newcommand{\VReduces}[2][\State]{\Reduces_{{#1},{#2}}}
\newcommand{\Stopped}[3][\TName]{{\mathrm{stopped}({#1},{#2},{#3})}\ }
\newcommand{\Bind}[2][\State]{\Reduces_{{#1},{#2}}}

\newcommand{\grmor}{|}
\newcommand{\Grmor}{\ \grmor\ }
\newcommand{\Grmeq}{::=}

\newcommand{\OP}[2][\TName]{{#1},{#2}}

\newcommand{\WRITE}[1]{\mathtt{write}\ {#1}}
\newcommand{\READ}[1]{\mathtt{read}\ {#1}}
\newcommand{\FUTURE}[1]{\mathtt{future}\ {#1}}
\newcommand{\FORCE}[1]{\mathtt{force}\ {#1}}
\newcommand{\TAU}{\tau}

\title{Language with futures}
\date{}

\begin{document}
\maketitle

\section{Language}


Numbers:

$$
\Nat \Grmeq \dots \Grmor 0 \Grmor 1 \Grmor 2 \Grmor \dots
$$

Words, where $\TName$ are task names and $\HName$ are heap names:

$$
\Word \Grmeq \Nat \Grmor \TName \Grmor \HName
$$

Run-time values, where $\Var$ are variable names:

$$
\Val \Grmeq \Word \Grmor \Var
$$

Expressions:

$$
\begin{aligned}
\Exp    \Grmeq & \Val  \\
        \Grmor & \Deref \\
        \Grmor & \Malloc \\
        \Grmor & \Future {\vec \Val}  {\vec \Var} \Prog \\
        \Grmor & \Force 
\end{aligned}
$$

Instructions:

$$
\Inst \Grmeq \Var = \Exp \Grmor \Store \Exp
$$

Programs:

$$
\Prog \Grmeq \Inst; \Prog \Grmor \If \Prog \Prog \Grmor \Ret
$$

\section{Abstract machine}

Operations:
$$
\Op \Grmeq \READ \HName \Grmor \WRITE \HName \Grmor  \FUTURE \TName \Grmor \FORCE \TName \Grmor \TAU
$$

Local store:

$$
\sigma ::= \{\Var_1:\Word_1,\dots,\Var_n:\Word_n\}
$$

Task:

$$
\Task \Grmeq (\Local, \Prog)
$$

Task map:

$$
\TaskMap ::= \{\TName_1:\Task_1,\dots,\TName_n:\Task_n\}
$$

Heap values (words or undefined):

$$
\HeapVal \Grmeq \Word \Grmor ?
$$

Heap:

$$
\HeapMap ::= \{\HName_1\colon \HeapVal_1,\dots,\HName_n\colon \HeapVal_n\}
$$

State:

$$
\State ::= (\HeapMap,\TaskMap)
$$

\noindent
\textbf{Task memory:}\quad\fbox{$\GetLocal \TName  \Local$}
$$
\frac{
  \TaskMap(\State)(\TName) \mapsto (\Local,\Prog)
}{
  \GetLocal\TName \Local
}
$$

\noindent
\textbf{Program:}\quad\fbox{$\Program \TName \Prog$}
$$
\frac{
  \TaskMap(\State)(\TName) \mapsto (\Local,\Prog)
}{
  \Program \TName \Prog
}
$$


\noindent
\textbf{Reduces value:}\quad\fbox{$\Val \VReduces \TName \Word$}
  %
  $$
  \frac{
    \GetLocal\TName  \Local \qquad \Local(\Var) \mapsto \Word
  }{
    \Var \VReduces \TName \Word
  }
  \qquad
  \Word \VReduces \TName \Word
  $$
  %
 
\noindent
\textbf{Stopped:}\quad\fbox{$ \Stopped \State \Word$}
  %
  $$
  \frac{
    \Program \TName \Ret
    \qquad
    \Val \VReduces \TName \Word
  }{
     \Stopped \State \Word
  }
  $$

\noindent
\textbf{Bind:}\quad\fbox{$(\vec\Val,\vec\Var) \Bind \TName \Local$}
  %
  $$
  \frac{
    \forall i \in \{1,\dots,n\} \colon \Val_i \VReduces \TName \Word_i
  }{
    (\Val_1\cdots\Val_n, \Var_1\cdots\Var_n)  \Bind \TName \{\Var_1\colon \Word_1,\dots,\Var_n\colon\Word_n\}
  }
  $$
  %

  \noindent
  \textbf{Get expression from instruction:}\quad\fbox{$\Inst[\Exp]$}
  %
  $$
  (\Store \Exp)[\Exp]
  \qquad
  (\Var = \Exp)[ \Exp]
  $$
  %

\noindent
  \textbf{Reduces expressions:}\quad \fbox{$(\State,\Exp) \EReduces \Op  (\State,\Val)$}
  \begin{gather*}
  \frac{
    \Val \VReduces \TName \HName
    \qquad
    \HeapMap(\State)(\HName) \mapsto \Word
  }{
    (\State,\Deref) \EReduces {\READ \HName} (\State,\Word)
  }
  \qquad
  \frac{
    \HName \notin \HeapMap(\State)
  }{
    (\State,\Malloc) \EReduces {\TAU} (\putGlobal \HName ? \State,\HName)
  }
  \\
  \frac{
    (\vec\Val,\vec\Var) \Bind \TName \Local
    \qquad
    \TName' \notin \TaskMap(\State)
  }{
    (\State,\Future {\vec\Val} {\vec\Var} \Prog) \EReduces {\FUTURE {\TName'}} (\spawn {\TName'} {\Local} {\Prog} \State,\TName')
  }
  \qquad
  \frac{
    \Val \VReduces \TName {\TName'}
    \qquad
     \Stopped[\TName'] \State \Word
  }{
    (\State,\Force) \EReduces {\FORCE {\TName'}} (\State,\Word)
  }
  \end{gather*}


  \noindent
  \textbf{Reduces instructions:}\quad \fbox{$(\State,\Inst) \IReduces \Op \State$}
  \begin{gather*}
  \frac{
    \Val \VReduces \TName \HName
    \qquad
    \Valy \VReduces \TName \Word
  }{
    (\State,\Store \Valy) \EReduces {\WRITE {\HName}} {\putGlobal {\HName} {\Word} \State}
  }
  \qquad
  \frac{
    \Val \VReduces \TName \Word
  }{
    (\State,\Var = \Val) \EReduces {\TAU} {\putLocal \TName \Var \Word \State}
  }
  \end{gather*}

  \noindent
  \textbf{Reduces programs:}\quad \fbox{$(\State,\Prog) \PReduces \Op (\State,\Prog)$}
  \begin{gather*}
    \frac{
      \Inst[\Exp]
      \qquad
      (\State,\Exp) \EReduces \Op (\State',\Word)
    }{
      (\State,\Inst;\Prog) \PReduces \Op (\State',\EEval \Inst \Word;\Prog)
    }
    \qquad
    \frac{
      (\State,\Inst) \IReduces \Op \State'
    }{
      (\State,\Inst;\Prog) \PReduces \Op (\State',\Prog)
    }
    \\
    \frac{
    \Val \VReduces \TName 0
    }{
      (\State,\If {\Prog} {\Prog'}) \PReduces \TAU (\State,\Prog')
    }
    \qquad
    \frac{
    \Val \VReduces \TName \Nat
    \qquad
    \Nat \neq 0
    }{
      (\State,\If {\Prog} {\Prog'}) \PReduces \TAU (\State,\Prog)
    }
  \end{gather*}  

  \noindent
  \textbf{Reduces states:}\quad \fbox{$\State \SReduces {\OP{\Op}} \State$}
  \begin{gather*}
    \frac{
      (\State,\Prog) \PReduces \Op (\State',\Prog')
    }{
      \State \SReduces {\OP{\Op}} \setProg \TName {\Prog'} {\State'}
    }
  \end{gather*}

\section{Race detection}

Node (from the computation-graph):

$$
\Node \Grmeq (\TName,\Nat)
$$

Edge:

$$
\Edge \Grmeq (\Node,\Node)
$$

Set of edges:

$$
\Edges \Grmeq \{ \Edge_1,\dots,\Edge_n\}
$$

Set of nodes:

$$
\Nodes \Grmeq \{ \Node_1,\dots,\Node_n\}
$$

Time:
$$
\Time \Grmeq \{ \TName_1 \colon \Nat_1, \dots, \TName_n\colon \Nat_n\}
$$



Read and write accesses:

$$
\Access \Grmeq (\Nodes,\Nodes)
$$

Access map (shadow memory):

$$
\AccessMap \Grmeq \{ \HName_1\colon \Access_1,\dots,\HName_n\colon\Access_n\}
$$

Computation graph reduction \fbox{$\CG \reduces[{\OP{\Op}}] \CG$}:

\begin{gather*}  
\frac{
  \Time(\TName) \mapsto \Node_1
  \qquad
  \Node'_1 \notin \Edges
  \qquad
  \Node_2 \notin \Edges
  \qquad
  \TName' \notin \Time
}{
  (\Time, \Edges)
  \reduces[{\OP{\FUTURE \TNamey}}] 
  (\Time, \TName \colon \Node'_1, \TNamey \colon \Node_2, \Edges \cup \{(\Node_1,\Node_2), (\Node_1,\Node_1') \})
}
\\
\frac{
  \Time(\TName) \mapsto \Node_1
  \qquad
  \Time(\TNamey) \mapsto \Node_2
  \qquad
  \Node'_1 \notin \Edges
}{
  (\Time, \Edges)
  \reduces[{\OP{\FORCE \TNamey}}]
  (\Time, \TName \colon \Node_1', \Edges \cup \{(\Node_2,\Node_1'), (\Node_1,\Node_1')\}
}
\\
\frac{
  \forall \TNamey, \Op \neq \FORCE \TNamey
  \qquad
  \forall \TNamey, \Op \neq \FUTURE \TNamey
}{
  \CG \reduces[{\OP{\Op}}] \CG
}
\end{gather*}

Shadow memory \fbox{$(\CG,\AccessMap) \reduces[{\OP{\Op}}] \AccessMap$}:

\begin{gather*}
\frac{
  \Time(\TName) \mapsto \Nat
  \qquad
  \AccessMap(\HName) \mapsto (\Nodes_r,\Nodes_w)
}{
  ((\Time,\Edges), \AccessMap) \reduces[{\OP{\WRITE \HName}}] \AccessMap, \HName \colon (\Nodes_r,\Nodes_w \cup \{(\TName,\Nat)\})
}
\\
\frac{
  \Time(\TName) \mapsto \Nat
  \qquad
  \AccessMap(\HName) \mapsto (\Nodes_r,\Nodes_w)
}{
  ((\Time,\Edges), \AccessMap) \reduces[{\OP{\READ \HName}}] \AccessMap, \HName \colon (\Nodes_r\cup \{(\TName,\Nat)\},\Nodes_w )
}
\\
\frac{
  \forall \HName, \Op \neq \READ \HName
  \qquad
  \forall \HName, \Op \neq \WRITE \HName
}{
  (\CG, \AccessMap) \reduces[{\OP{\Op}}] \AccessMap
}
\end{gather*}

The whole thing:
\begin{gather*}
\frac{
  \State \reduces[{\OP{\Op}}] \State'
  \qquad
  \CG \reduces[{\OP{\Op}}] \CG'
  \qquad
  (\CG, \AccessMap) \reduces[{\OP{\Op}}] \AccessMap
}{
  (\State,\CG,\AccessMap)
  \reduces
  (\State',\CG',\AccessMap')
}
\end{gather*}
\end{document}