prezentace.tex

\documentclass[10pt]{beamer}

\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{beamerthemebars}

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{mathpazo}
\usepackage{upgreek}
\usepackage[czech]{babel}
\usepackage{fontenc}
\usepackage{graphicx}

\author{Jan Kriho}
\title{Post-mortem analýza stavového prostoru}
\date{jaro 2011}

\PrerenderUnicode{ž}
\PrerenderUnicode{ý}
\PrerenderUnicode{é}

\begin{document}


 \begin{frame}
  \titlepage
 \end{frame}

\begin{frame}{Obsah}
 \tableofcontents
\end{frame}


\section{Model Checking}
\begin{frame}{Co to je model checking}
 \begin{itemize}
  \item Metoda formální verifikace
\item Hledání negativních akceptujících cyklů
 \end{itemize}

\end{frame}

\begin{frame}{Prostředky pro model checking}
 \begin{itemize}
  \item Kripkeho struktury
  \item LTL
  \item Büchiho automaty
 \end{itemize}

\end{frame}



\section{DiVinE}
\begin{frame}{DiVinE}
 Co je to DiVinE?
\begin{itemize}
 \item Implementace formálních metod model checkingu
\item Vyvíjen laboratoří ParaDiSe na FI MUNI
\item Nejnovější verze 2.5.1

\end{itemize}

\end{frame}

\subsection{Datové struktury}
\begin{frame}{Struktura DiVinE}
 \begin{center}
 \includegraphics[bb=0 0 595 842,keepaspectratio=true,clip=true,trim=100pt 0pt 000pt 100pt,width=400pt]{./divine_orig.pdf}
% divine_orig.pdf: 595x842 pixel, 72dpi, 20.99x29.70 cm, bb=0 0 595 842

\end{center}

\end{frame}

\begin{frame}{Graph}
Rozhraní grafu:
 \begin{itemize}
  \item read, setSlack
  \item initial, queueInitials
  \item successors
  \item showNode
 \end{itemize}

\end{frame}

\begin{frame}{HashSet}
 Rozhraní úložiště:
\begin{itemize}
 \item insert
 \item get, has, operator[]
\end{itemize}

\end{frame}



% \subsection{Algoritmy}
% \begin{frame}
% Sekvenční algoritmy
% \begin{itemize}
%  \item Nested DFS
% \end{itemize}
% Distribuované algoritmy
% \begin{itemize}
%  \item Metrics
%  \item Reachability
%  \item OWCTY, MAP...
% \end{itemize}
% \end{frame}

\subsection{Komunikace mezi procesy}

\begin{frame}{Komunikace mezi procesy}
 \begin{center}
 \includegraphics[bb=0 0 595 842,keepaspectratio=true,clip=true,trim=80pt 0pt 000pt 135pt,width=450pt]{./divine_networking.pdf}
% divine_orig.pdf: 595x842 pixel, 72dpi, 20.99x29.70 cm, bb=0 0 595 842

\end{center}
\end{frame}


\begin{frame}{DomainWorker}
Rozhraní správce paralelizace
 \begin{itemize}
  \item becomeMaster, peers
  \item idle, workWaiting, restart
  \item comms
 \end{itemize}

\end{frame}

\begin{frame}{FifoMatrix}
 Rozhraní komunikačních kanálů
\begin{itemize}
 \item pending
 \item submit
 \item take
\end{itemize}

\end{frame}






\section{Ukládání stavového prostoru}

\subsection{Motivace a požadavky}

\begin{frame}{Motivace}
 Proč ukládat stavový prostor
\begin{itemize}
 \item Analýza protipříkladu
 \item Analýza výsledného grafu
 \item Analýza a ladění verifikačních algoritmů
\end{itemize}
\end{frame}
\begin{frame}{Požadavky}
\begin{itemize}

 \item \textbf{Možnost rekonstrukce stavového prostoru v podobě grafu}

 \item Zachování výhod distribuovaného systému

 \item Přenositelnost mezi architekturami

 \item Možnost rekonstrukce co nejvíce aspektů běhu algoritmu

\end{itemize}

\end{frame}
\subsection{Princip}
\begin{frame}{Princip ukládání}
 \begin{center}
 \includegraphics[bb=0 0 595 842,keepaspectratio=true,clip=true,trim=100pt 0pt 000pt 100pt,width=400pt]{./divine_new.pdf}
% divine_orig.pdf: 595x842 pixel, 72dpi, 20.99x29.70 cm, bb=0 0 595 842

\end{center}


\end{frame}

\subsection{Formát souboru}
\begin{frame}{Formát souboru}
 \begin{columns}
  \column{.5\textwidth}
\only<1>{

Hlavička:

\begin{enumerate}
 \item Použitý generátor a algoritmus
 \item Stupeň paralelizace
 \item Počet iniciálních vrcholů
 \item Informace o architektuře
\end{enumerate}

}
\only<2>{
Seznam počátečních vrcholů:
\begin{center}
\begin{tabular}{|l|}\hline
Index vrcholu (8 B)\\\hline
Číslo tabulky (4 B)\\\hline
\end{tabular}
\end{center}

}

\only<3>{
Deskriptor tabulky:
\begin{enumerate}
 \item Offset tabulky
 \item Počet vrcholů
 \item Velikost dat
\end{enumerate}

}

  \column{.5\textwidth}
\begin{tabular}{|p{12em}|}\hline
Hlavička ($24 + 8$ B)\\\hline
Seznam počátečních vrcholů ($n * 12$ B)\\\hline
Deskriptory tabulek ($n*32$ B)\\\hline
Vlastní tabulky\\\hline
     \end{tabular}

 \end{columns}

\end{frame}

\begin{frame}{Formát souboru II -- Vlastní tabulky}

 \begin{columns}
  \column{.5\textwidth}
\only<1>{
Položka indexu vrcholů:
\begin{enumerate}
 \item Offset dat
 \item Offset následníků
 \item Atributy
\end{enumerate}
}

\only<2>{
Seznam následníků:
\begin{center}
\begin{tabular}{|l|}\hline
Index vrcholu (8 B)\\\hline
Číslo tabulky (4 B)\\\hline
\end{tabular}
\end{center}
}

\only<3>{
Data k vrcholu:
\begin{enumerate}
 \item Binární reprezenace vrcholu
\begin{itemize}
 \item Samotný popis vrcholu pro graf
 \item Data uložená generátorem a algoritmem
\end{itemize}
 \item Textová reprezentace vrcholu
\end{enumerate}

}


  \column{.5\textwidth}
\begin{tabular}{|p{12em}|}\hline
Index vrcholů ($n*28$ B)\\\hline
Seznam následníků ($n * 12$ B)\\\hline
Data k~vrcholům\\\hline

     \end{tabular}
 \end{columns}

\end{frame}


\section{Implementace}

\subsection{Sekvenční algoritmus}
\begin{frame}{Sekvenční algoritmus}
 \begin{enumerate}
  \item Linearizace úložiště stavů
  \item Získání následníků
  \item Zjištění iniciálních vrcholů
  \item Výpočet offsetů
  \item Samotné ukládání
 \end{enumerate}

\end{frame}

\subsection{Distribuovaný algoritmus}
\begin{frame}{Distribuovaný algoritmus}
\begin{enumerate}
  \item Linearizace úložiště stavů
  \item Získání následníků
  \item Zjištění iniciálních vrcholů
  \item Sesbírání deskriptorů tabulek
  \item Výpočet offsetů
  \item Sesbírání a ukládání tabulek
 \end{enumerate}

\end{frame}
\subsection{Výkon}

\begin{frame}{Porovnání výkonu s Compact}
\begin{itemize}
 \item divine metrics -r --dump-state-space examples/beem-peterson.4.dve [219 MB]
 \item divine compact -w 1 -r  examples/beem-peterson.4.dve [32 MB]
\end{itemize}
\begin{center}
\begin{tabular}{llll}
Algoritmus & Procesů & MPI & Čas\\
DSS & 1 & -- & 19 s\\
Compact & 1 & -- & 22 s\\
DSS & 2 & Ano & 25 s\\
Compact & 2 & Ano & 30 s\\
Compact & 2 & Ne & 25 s
\end{tabular}
\end{center}


\end{frame}

\begin{frame}{Aktuální kód}
Aktuální patch je k~dispozici na~adrese:
 \begin{center}
  http://erbureth.galaxyhosting.cz/divine.patch
 \end{center}

\end{frame}


\end{document}