tobast/talk-2019-10-OOPSLA19
1
0
Fork 0
forked from m2-internship/talk-2018-11-uppsala
Code Releases Activity

Changes made during rehearsal w/ Francesco

Browse source
This commit is contained in:
Théophile Bastian 2019-10-19 07:14:07 +02:00
parent cfd73303e6
commit d95da5ab8c
1 changed files with 20 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
slides.tex
View file

@ -176,7 +176,7 @@ Segmentation fault.
\end{lstlisting}
\pause{}
\begin{center}
\textbf{\Large How does it work?!}
\textbf{\Large How does it work?}
\end{center}
\end{column}
\begin{column}{0.35\textwidth}
@ -194,7 +194,8 @@ Segmentation fault.
\begin{column}{0.65\textwidth}
\begin{center}
\large\bf
How do we get the RA\@?
How do we get\\
the return address?
\vspace{2em}
@ -393,7 +394,7 @@ Segmentation fault.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Correct by construction unwinding tables: synthesis}
\section{Correctness by construction:\\*\textbf{synthesis of unwinding tables}}
\sectiontitleframe{}
\newcommand{\tblrowval}[4]{#1 & #2 & \only<2->{#3} & \only<2->{#4} \\}
@ -424,15 +425,16 @@ Segmentation fault.
{\only<3>{
\begin{textblock*}{0.90\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
\begin{textblock*}{\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
\begin{tcolorbox}[halign=center, colframe=red, colback=Lavender]
\large
\alert{\bf Assumptions:}
\alert{\bf Assumptions}
\vspace{0.6em}
\begin{itemize}
\item the assembly is was generated by a compiler
\item which also generated unwinding data
\item and I have a reliable DWARF interpreter
\item the compiler generated the unwinding data
\item we have a reliable DWARF interpreter
\end{itemize}
\end{tcolorbox}
\end{textblock*}
}}
@ -482,7 +484,8 @@ Segmentation fault.
\item Heuristic to decide whether we index with \reg{rbp} or
\reg{rsp}
\end{itemize}
\item By performing symbolic execution, we can \alert{synthesize the
\item By performing \alert{symbolic execution} with an abstract
semantics, we can \alert{synthesize the
unwinding table} line by line.
\item Control flow: forward data-flow analysis
\item The fixpoints are immediate, cf article
@ -579,12 +582,12 @@ Segmentation fault.
\begin{frame}
\begin{itemize}
\item \alert{libunwind}: \textit{de facto} standard library for
\item \alert{libunwind}: most common library for
unwinding
\bigskip{}
\item \texttt{libunwind-eh\_elf}: alternative implementation using
\item \alert{\texttt{libunwind-eh\_elf}}: modified version to support
\ehelfs{}
\item[$\leadsto$] Same API, almost \alert{``relink-and-play''} for existing projects!
@ -597,7 +600,7 @@ Segmentation fault.
\begin{frame}{Performances}
\begin{center}
\Large\bf Speedup vs. libunwind:
\Large\bf Unwinding speedup vs.\ libunwind:
\begin{columns}
\begin{column}{0.5\textwidth}
\alert{x15} on gzip
@ -635,8 +638,8 @@ Segmentation fault.
\item{} Synthesis + compare = verification of unwinding data!
\item{} Integrate synthesis into compilers \& debuggers\\
$\rightarrow$ support for inline assembly, fallback method, \ldots
\item{} Integrate into \prog{perf} for a faster analysis
\item{} Probably many more cool things to do!
\item{} Integrate into \prog{perf} for online unwinding
\item{} Probably many more cool projects!
\end{itemize}
\vspace{1em}
@ -715,15 +718,15 @@ Segmentation fault.
\vspace{1em}
We cannot hope for an invariant\dots\\
We cannot hope for a simple invariant\dots\\
but the compiler cannot
either.
\vspace{1em}
{
\large\alert{$\implies$} the compiler will \alert{fallback to
\reg{rbp}}\\
\large\alert{$\implies$} the compiler will\\
\alert{fallback to \reg{rbp}}\\
}
even with \lstbash{--fomit-frame-pointer}
\end{center}