Home My Page Projects Code Snippets Project Openings diderot

# SCM Repository

[diderot] View of /trunk/doc/semantics/semantics.tex
 [diderot] / trunk / doc / semantics / semantics.tex

# View of /trunk/doc/semantics/semantics.tex

Wed May 18 19:30:16 2011 UTC (8 years, 1 month ago) by lamonts
File size: 3893 byte(s)
Added the code for generating OpenCL
\documentclass[11pt]{article}

\input{defs}

\usepackage{graphicx}
\usepackage{fullpage}
\usepackage{amsfonts}

\title{Diderot Formal Semantics}
\author {
John Reppy \\
University of Chicago \\
{\small\tt{}jhr@cs.uchicago.edu} \\
\and
Lamont Samuels \\
University of Chicago \\
{\small\tt{}lamonts@cs.uchicago.edu} \\
}
\date{\today}

\begin{document}
\maketitle
\thispagestyle{empty}

\section{Abstract Syntax}

\noindent{}\point Definitions:  variable := string \textbar{} id := integer

\noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??

\noindent{}\point Commands (Comms):
\begin{displaymath}
\begin{array}{rclr}
\text{c} &  ::=  &\text{x := e}  & \text{for x = variable, e} \in\text{Aexp}\\
& \mid & \text{$c_1$;  $c_2$}  &\text{for $c_1$, $c_2$} \in\text{Comms} \\
& \mid & \text{$if\:r\:then\:c_1\:else\:c_2$}  &\text{for $c_1$, $c_2$} \in\text{Aexp and b} \in\text{Rexp}  \\
& \mid & \text{stabalize}
\end{array}
\end{displaymath}

\section{Strand Environment}
\begin{displaymath}
\begin{array}{l}
\noindent{}strand \US status  :=  \{ Active, Stabilized, Dead \}  \times{}  env \\
\noindent{}strand \US env := strand \US status \times{} id  \times{} comms \\
\noindent{}env := variable   \rightarrow{} value
\end{array}
\end{displaymath} %

\section{Global Environment}
The $\cup$ character denotes a parallel construct that states that every stand environment
runs in parallel with each other.

\begin{center}
$\displaystyle \bigcup_{\substack {id \in strand\_env \\ \Gamma = id \rightarrow strand\_env} }{update(\Gamma(id),\Gamma)}$
\end{center}
\vspace{12pt}
dom($\Gamma$) := all active \& stabilized strand environments

\noindent{}newId := $\Gamma$ * id $\rightarrow$ id

\section{Inference Rules}

\noindent{}\point Update function: strand\_env * $\Gamma \rightarrow \Gamma'$
\vspace{12pt}
%\begin{center}

%$\INFER{update((Active,env),id,c),\Gamma)\Downarrow \Gamma'[(new\_status,env')/id]} % {comm\_eval((Active,env),c,id,\Gamma) \Downarrow (new\_status,env',\Gamma')}$

%\end{center}

%\vspace{12pt}
%\noindent{}\point comm\_eval: strand\_status * commands * id * $\Gamma \rightarrow$  strand\_status * env * $\Gamma'$
\vspace{12pt}

\begin{center}
\CommEval{stabalize}{(Stablize,env,\Gamma)}{}

%$\INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$
%\vspace{24pt}

%$\INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$
%\vspace{24pt}
% $\INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{\ExpEval{env}{e}{v}}$
%\vspace{24pt}

%\CommEval{c_1; c_2}{(s'',env'',\Gamma'')}{\ExpEval{c_1} {(s,env) + \Gamma)} {(s',env',\Gamma')}}

%$\INFER{comm\_eval((s,env),c_1; c_2,id,\Gamma)\Downarrow (s',env'',\Gamma'')} % {comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma') \hspace{.2in} comm\_eval((s',env),c_2,\Gamma') \Downarrow (s'',env'',\Gamma'')}$
%\vspace{24pt}

$\INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,id,\Gamma)\Downarrow (s',env',\Gamma')} {rel\_op(b,env) \Downarrow Bool(true) \hspace{.2in} comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma')}$
\vspace{24pt}

$\INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,\Gamma)\Downarrow (s',env',\Gamma')} {rel\_op(b,env) \Downarrow Bool(false) \hspace{.2in} comm\_eval((s,env),c_2,\Gamma) \Downarrow (s',env',\Gamma')}$
\vspace{24pt}

$\INFER{comm\_eval((s,env), spawn,id,\Gamma)\Downarrow (s,env,\Gamma[id'])} {newId(\Gamma,id) \Downarrow id'}$

\end{center}

\vspace{12pt}
\noindent{}\point expr\_eval:  Aexp * $\Gamma \rightarrow$ v
\vspace{12pt}

\noindent{}\point rel\_op:  Rexp * $\Gamma \rightarrow$ Bool(b)
\vspace{12pt}

\end{document}