source: CIVL/doc/tutorial/tutorial.tex@ 0c65483

\documentclass[t]{beamer}
\input{preambular}
\foot{CIVL Tutorial}
\date{\today}
\title{{\huge\bf CIVL}\\
  Concurrency Intermediate Verification Language\\ \ \\
  Tutorial}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

\begin{frame}{What is CIVL?}
  CIVL is \ldots
  \begin{enumerate}
  \item \ldots a programming language, \alert{CIVL-C}
    \begin{itemize}
    \item based on subset of C
    \item extensions for concurrency, naming of scopes
    \end{itemize}
  \item \ldots a suite of tools for analyzing CIVL-C programs
    \begin{itemize}
    \item running + dynamic checking
    \item model checking
    \item static analyses (coming)
    \end{itemize}
  \item \ldots a set of translators from common programming
    language/concurrency API combinations to CIVL-C
    \begin{itemize}
    \item coming
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}[containsverbatim]{Example: \code{adder.cvl}}

  \begin{tabular}[t]{l|l}
    \begin{minipage}[t]{.45\textwidth}\scriptsize
\begin{verbatim}
#include <civlc.h>

$input int B;
$input int N;
$assume 0<=N && N<=B;
$input double a[N];

double adderSeq(double *p, int n) {
  double s = 0.0;
  
  for (int i = 0; i < n; i++)
    s += p[i]; 
  return s;
}

double adderPar(double *p, int n) {
  double s = 0.0;
  _Bool mutex = 0;
  $proc workers[n];

  void worker(int i) {
    double t;
\end{verbatim}
    \end{minipage}
    &
    \begin{minipage}[t]{.45\textwidth}\scriptsize
\begin{verbatim}
    $when (mutex == 0) mutex = 1;
    t = s;
    t += p[i];
    s = t;
    mutex = 0;
  }
  
  for (int j = 0; j < n; j++)
    workers[j] = $spawn worker(j);
  for (int j = 0; j < n; j++)
    $wait workers[j];
  return s;
}

void main() {
  double seq = adderSeq(&a[0], N);
  double par = adderPar(&a[0], N);

  $assert seq == par;
}
\end{verbatim}
    \end{minipage}
  \end{tabular}
\end{frame}

\begin{frame}[containsverbatim]{Verifying \code{adder.cvl}}

\begin{verbatim}
concurrency$ civl verify -inputB=5 adder.cvl
CIVL v0.4 of 2013-12-06 -- http://vsl.cis.udel.edu/civl
=================== Stats ===================
   validCalls          : 23883
   proverCalls         : 29
   memory (bytes)      : 374341632
   time (s)            : 5.35
   maxProcs            : 6
   statesInstantiated  : 28761
   statesSaved         : 3082
   statesSeen          : 3082
   statesMatched       : 1968
   transitions         : 5049

The standard properties hold for all executions.
concurrency$
\end{verbatim}
\end{frame}

\begin{frame}{Download and Installation}
  \begin{enumerate}
  \item Get a Java 7 VM.
  \item Go to \url{http://vsl.cis.udel.edu/civl}
  \item Navigate to downloads, \emph{latest stable release}.
  \item Download version corresponding to your platform.
    \begin{itemize}
    \item for now, pre-compiled versions for OS X and linux (32- and 64-bit)
    \item other platforms must build from source
    \end{itemize}
  \item Unpack and move resulting directory \texttt{CIVL-\textit{tag}}
    under \texttt{/opt}.
  \item Download the VSL dependencies archive.
    \begin{itemize}
    \item contains a number of pre-compiled open source libraries used by CIVL
    \item \url{http://vsl.cis.udel.edu/tools/vsl\_depend}
    \end{itemize}
  \item Unpack and move resulting directory \texttt{vsl} under \texttt{/opt}.
  \item Put \texttt{/opt/CIVL-\textit{tag}/bin/civl} in your path.
    \begin{itemize}
    \item however you want: move it, symlink, \ldots
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}[containsverbatim]{Test your installation}

  From command line \ldots

\begin{verbatim}
concurrency$ civl
CIVL v0.4 of 2013-12-06 -- http://vsl.cis.udel.edu/civl
Missing command
Type "civl help" for command line syntax.

concurrency$ civl help
...
\end{verbatim}

Copy \texttt{/opt/CIVL-\textit{tag}/examples/concurrency/adder.cvl}
to your working directory and try

\begin{verbatim}
    civl verify -inputB=5 adder.cvl
\end{verbatim}
\end{frame}

\begin{frame}{What features are inherited from C?}
  \begin{itemize}
  \item most syntax
  \item types
    \begin{itemize}
    \item \texttt{{\U}Bool} $\ra$ $\{0,1\}$
    \item \texttt{int}, \texttt{long}, \texttt{short}, \ldots $\ra$ $\Z$
    \item \texttt{double}, \texttt{float}, \ldots $\ra$ $\R$
    \item structure, array, pointer, and function types
    \end{itemize}
  \item expressions
    \begin{itemize}
    \item addition, multiplication, division, subtraction, unary minus (\code{+}, 
      \code{*}, \code{/}, \code{-})
    \item integer division (\code{/}) and modulus (\code{\%})
    \item pointer dereference (\code{*}), address-of (\code{\&})
    \item array subscript (\code{[...]})
    \item structure navigation (\code{.})
    \item logical and (\code{\&\&}), or (\code{||}), not (\code{!})
    \item \code{==}, \code{!=}, \code{<}, \code{>}, \code{<=}, \code{>=}
    \item pointer addition (\code{+}) and subtraction (\code{-})
    \item \code{++}, \code{--}
    \item \alert{no bit-wise operations} for now
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Inherited from C, cont.}
  \begin{itemize}
  \item statements
    \begin{itemize}
    \item no-op, labeled-statement, compound-statement
    \item assignments (\code{=}, \code{+=}, \code{-=}, \ldots)
    \item function call
    \item \code{if}\ldots\code{else}
    \item \code{goto}, \code{while}, \code{do}, \code{for},
      \code{switch}, \code{break}
    \end{itemize}
  \item procedure (function) prototypes and definitions
  \item \code{typedef}
  \item preprocessing directives
  \end{itemize}
\end{frame}

\begin{frame}{New features}
  \begin{itemize}
  \item functions can be declared in any scope
  \item concurrency primitives
    \begin{itemize}
    \item spawning processes, waiting for a process to terminate, guarded commands
    \item nondeterministic choice
    \item explicit naming of scopes
    \item scope-parameterized pointers
    \item other primitives useful for verification
      \begin{itemize}
      \item input qualifier, assert, assume, procedure contracts
      \end{itemize}
    \end{itemize}
  \item library-level constructs supporting message-passing, \ldots
  \end{itemize}
\end{frame}

\begin{frame}{Some CIVL-C primtives}
  \begin{tabular}{ll}
    \cproc & the process type \\
    \cself & the evaluating process (constant of type \cproc) \\
    \cscope & the scope type \\
    \cinput & type qualifier declaring variable to be a program input \\
    \coutput & type qualifier declaring variable to be a program output \\
    \cspawn & create a new process running procedure \\
    \cwait & wait for a process to terminate \\
    \cassert & check something holds \\
    \ctrue & boolean value true, used in assertions \\
    \cfalse & boolean value false, used in assertions \\
    \cassume & assume something holds \\
    \cwhen & guarded statement \\
    \cchoose & nondeterministic choice statement \\
    \cchooseint & nondeterministic choice of integer
  \end{tabular}
\end{frame}

\begin{frame}{CIVL Command line tools}
  \begin{itemize}
  \item \code{civl run filename}
    \begin{itemize}
    \item run the CIVL program making nondeterministic choices randomly
    \item \code{-seed=LONG} : use this random seed (reproducible)
    \end{itemize}
  \item \code{civl verify filename}
    \begin{itemize}
    \item explore reachable state space, checking properties at each state
      \begin{itemize}
      \item absence of deadlock, assertion violations, division by $0$,
        invalid pointer dereference, out of bounds array access, \ldots
      \end{itemize}
    \item may specify bounds using \cinput{} variables and command line
      \begin{itemize}
      \item \code{-inputX=value}
      \end{itemize}
    \item \code{-errorBound=INT} specifies maximum number of errors that
      will be logged before quitting
    \end{itemize}
  \item \code{civl replay}
    \begin{itemize}
    \item  if a violation was found during \code{verify}, its trace
      is saved to a file; this will run the trace
    \item \code{-id=INT} can be used to specify the ID of the trace if more than one
    \item \code{-trace=tracefile} can be used to specify the exact filename 
      containing trace
    \end{itemize}
  \end{itemize}  
\end{frame}

\begin{frame}{Scope-parameterized pointers}
  \begin{itemize}
  \item a declaration of the form \code{\cscope\ s;} assigns the name
    \code{s} to the containing scope
    \begin{itemize}
    \item what you can do with \code{s} is very limited
    \item cannot be assigned, passed as parameter
    \end{itemize}
  \item \code{int *<s> p;}
    \begin{itemize}
    \item declares \code{p} to have type ``pointer-to-\code{int}-in-\code{s}''
    \item \code{p} can only hold a pointer to an object in scope \code{s}
    \end{itemize}
  \end{itemize}
\end{frame}


% static type checking

% subtype

% semantics ?

% scope-parameterized functions

% APIs for malloc, free, memcpy

% bundles

% message passing

\begin{frame}[containsverbatim]{Message Passing example: \code{ring.cvl}}

\begin{verbatim}
/* Create nprocs processes.  Have them exchange data
 * in a cycle.  Commandline example:
 *     civl verify -inputNPROCS=3 ring.cvl -simplify=false
 */
#include<civlc.h>
#include "mp_root.cvh"

void MPI_Process (int rank) {
#include "mp_proc.cvh"

  double x=rank, y;

  send(&x, 1, (rank+1)%NPROCS, 0);
  recv(&y, 1, (rank+NPROCS-1)%NPROCS, 0);
  $assert y==(rank+NPROCS-1)%NPROCS;
}
\end{verbatim}
\end{frame}

\begin{frame}[containsverbatim]{File \code{mp{\U}root.cvh}}
  \scriptsize
\begin{verbatim}
$input int NPROCS;
$proc __procs[NPROCS];
_Bool __start = 0;
$comm MPI_COMM_WORLD;

void MPI_Process (int rank);

void init() {
  for (int i=0; i<NPROCS; i++)
    __procs[i] = $spawn MPI_Process(i);
  MPI_COMM_WORLD = $comm_create(NPROCS, __procs);
  __start=1;
}

void finalize() {
  for (int i=0; i<NPROCS; i++)
    $wait __procs[i];
}

void main() {
  init();
  finalize();
}
\end{verbatim}
\end{frame}

\begin{frame}[containsverbatim]{File \code{mp{\U}proc.cvh}}
  \scriptsize
\begin{verbatim}
  void send(void *buf, int count, int dest, int tag) {
    $message out = $message_pack(rank, dest, tag, buf, count*sizeof(double));
    $comm_enqueue(&MPI_COMM_WORLD, out);
  }

  void recv(void *buf, int count, int source, int tag) {
    $message in = $comm_dequeue(&MPI_COMM_WORLD, source, rank, tag);
    $message_unpack(in, buf, count*sizeof(double));
  }

  $when (__start);
\end{verbatim}
\end{frame}

\begin{frame}{VSL Projects: Uses Relation}

  \includegraphics{vsl_projects}

  \begin{itemize}
  \item reusable components
    \begin{itemize}
    \item ABC: A Better C compiler?  ANTLR-Based C compiler?
    \item SARL: Symbolic Algebra \& Reasoning Library
    \item GMC: Generic Model Checking utilities
      \begin{itemize}
      \item DFS, command line interface, trace saving/replay, error
        logging, random simulation
      \end{itemize}
    \end{itemize}
  \item model checking applications
    \begin{itemize}
    \item CIVL: Concurrency Intermediate Verification Language
    \item TASS: Toolkit for Accurate Scientific Software (C+MPI)
    \item CVT: Chapel Verification Tool
    \end{itemize}
  \end{itemize}

\end{frame}

\begin{frame}{Engineering}

  \begin{itemize}
  \item all of the VSL software is in Java
  \item try to maintain coding standards
  \item clear module boundaries with interfaces
  \end{itemize}
  
  
  \begin{center}
    \begin{tabular}{|ll|}
      \hline
      Web page & \url{http://vsl.cis.udel.edu/civl}\\
      Subversion & \url{svn://vsl.cis.udel.edu/civl}\\
      Trac repository & \url{https://vsl.cis.udel.edu/trac/civl}\\
      Automated build/test & \url{http://vsl.cis.udel.edu/civl/test}\\
      \hline
    \end{tabular}
  \end{center}

  \begin{itemize}
  \item replace \texttt{civl} with \texttt{sarl}, \texttt{abc}, \texttt{gmc}, or
    \texttt{tass}
  \end{itemize}

  \includegraphics[scale=.3]{civl-trac.pdf}

\end{frame}

\begin{frame}{Automated Build \& Test Script}

  \begin{center}
    \includegraphics[scale=.3]{sarl-junit.pdf}
  \end{center}

  For each project \ldots
  \begin{itemize}
  \item script is run after each commit
  \item one directory for each \alert{branch} and \alert{trunk}
    \begin{itemize}
    \item one subdirectory for each revision, up to some bounded history
    \end{itemize}
  \item compiles all code and displays results
  \item runs JUnit test suite and displays results
  \item runs Jacoco coverage anaysis and displays results
  \item generates javadocs
  \end{itemize}
\end{frame}

\begin{frame}{Developer Eclipse Set-up}
  \begin{enumerate}
  \item Download vsl dependencies archive from
    \url{http://vsl.cis.udel.edu/tools/vsl_depend}
  \item Download and install Eclipse IDE for Java EE Developers
    \begin{itemize}
    \item version Kepler or later
    \end{itemize}
  \item Install Apache Ant if you don't have it
  \item Install an Eclipse SVN plugin (such as Subversive)
  \item Create class path variable \texttt{VSL}:
    \begin{itemize}
    \item Preferences$\ra$Java$\ra$Build Path$\ra$ClassPath Variables
    \item select ``New'' and create a classpath variable \texttt{VSL}
    \item specify its value to be \texttt{/opt/vsl}
    \end{itemize}
  \item Create string variable \texttt{vsl{\U}lib}:
    \begin{itemize}
    \item Preferences$\ra$Run/Debug$\ra$String Substitution$\ra$New
    \item define an entry \texttt{vsl{\U}lib}
    \item set its value to be \texttt{/opt/vsl/lib}
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}{Check out and install ABC}
  \begin{enumerate}
  \item Check out ABC Eclipse project 
    \begin{itemize}
    \item ``New Project\ldots from SVN''
    \item SVN repository: \url{svn://vsl.cis.udel.edu/abc}
    \item Navigate and select \texttt{trunk} from within archive
    \item Check out project using all default options
    \end{itemize}
  \item Build using Ant
    \begin{itemize}
    \item right-click on \texttt{build.xml}
    \item Choose ``Run as Ant build''
    \item Clean project
    \end{itemize}
  \item test the build
    \begin{itemize}
    \item select Run$\ra$Run Configurations\ldots
    \item ceate a new JUnit 4 configuration called ``ABC Tests''
    \item select ``Run all tests in the selected project\ldots''
    \item navigate and select the \texttt{test} folder in the ABC project
    \item under the Arguments tab, type \texttt{-ea} into the VM arguments field
    \item click ``Run'' to run the tests
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}{Check out and install GMC}
  \begin{enumerate}
  \item Check out GMC Eclipse project 
    \begin{itemize}
    \item ``New Project\ldots from SVN''
    \item SVN repository: \url{svn://vsl.cis.udel.edu/gmc}
    \item Navigate and select \texttt{trunk} from within archive
    \item Check out project using all default options
    \end{itemize}
  \item test the build
    \begin{itemize}
    \item select Run$\ra$Run Configurations\ldots
    \item ceate a new JUnit 4 configuration called ``GMC Tests''
    \item select ``Run all tests in the selected project\ldots''
    \item navigate and select the \texttt{test} folder in the GMC project
    \item under the Arguments tab, type \texttt{-ea} into the VM arguments field
    \item click ``Run'' to run the tests
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}{Check out and install SARL}
  \begin{enumerate}
  \item Check out SARL Eclipse project 
    \begin{itemize}
    \item ``New Project\ldots from SVN''
    \item SVN repository: \url{svn://vsl.cis.udel.edu/sarl}
    \item Navigate and select \texttt{trunk} from within archive
    \item Check out project using all default options
    \end{itemize}
  \item test the build
    \begin{itemize}
    \item select Run$\ra$Run Configurations\ldots
    \item ceate a new JUnit 4 configuration called ``SARL Tests''
    \item select ``Run all tests in the selected project\ldots''
    \item navigate and select the \texttt{test} folder in the SARL project
    \item under Arguments tab, type \texttt{-ea} into the VM arguments field
    \item under Environment tab, create an entry
      \texttt{DYLD{\U}LIBRARY{\U}PATH} (OS X) or
      \texttt{LD{\U}LIBRARY{\U}PATH} (linux), specify its value by
      clicking Variables, choose \texttt{vsl{\U}lib} from the list
    \item click ``Run'' to run the tests
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}{Check out and install CIVL}
  \begin{enumerate}
  \item Check out CIVL Eclipse project 
    \begin{itemize}
    \item ``New Project\ldots from SVN''
    \item SVN repository: \url{svn://vsl.cis.udel.edu/civl}
    \item Navigate and select \texttt{trunk} from within archive
    \item Check out project using all default options
    \end{itemize}
  \item test the build
    \begin{itemize}
    \item select Run$\ra$Run Configurations\ldots
    \item ceate a new JUnit 4 configuration called ``CIVL Tests''
    \item select ``Run all tests in the selected project\ldots''
    \item navigate and select the \texttt{test} folder in the CIVL project
    \item under Arguments tab, type \texttt{-ea} into the VM arguments field
    \item under Environment tab, create an entry
      \texttt{DYLD{\U}LIBRARY{\U}PATH} (OS X) or
      \texttt{LD{\U}LIBRARY{\U}PATH} (linux), specify its value by
      clicking Variables, choose \texttt{vsl{\U}lib} from the list
    \item click ``Run'' to run the tests
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}{CIVL modules}
  \begin{tabular}{@{}ll@{}}
    \includegraphics[scale=0.55]{civlModules}
    &
    \includegraphics[scale=.3]{civlEclipseModules}
  \end{tabular}
\end{frame}

\end{document}