Context Navigation

Changeset 131 for docs


Ignore:
Timestamp:
Dec 29, 2007, 6:04:00 PM (18 years ago)
Author:
neil.c.c.brown
Message:

Added various changes from the past few days; most of the content is now in place

File:
1 edited

Legend:

Unmodified
Added
Removed

  • docs/trunk/omega-test-slides/omega-test.tex

    r126 r131
    2626
    2727\title{Tock}
    28\subtitle{(削除) Omega is just the beginning (削除ここまで)}
    28\subtitle{(追記) Beginning with Omega (追記ここまで)}
    2929
    3030\author{Neil Brown}
    … …
    101101\end{frame}
    102102
    103%TODO mention occam STOPping on integer overflow and array out of bounds being very useful
    103\begin{frame}[fragile]
    104\frametitle{Occam}
    105\begin{itemize}
    106\item Integer overflow would make life complicated
    107 \begin{itemize}
    108 \item But this is a run-time error in occam!
    109 \end{itemize}
    110\item We check if indices can clash within the array bounds
    111 \begin{itemize}
    112 \item That is, we constrain the indices to be within bounds
    113 \item Out-of-bounds is also a run-time error in occam, anyway
    114 \end{itemize}
    115\end{itemize}
    116\end{frame}
    104117
    105118%TODO mention that we want integer solutions
    106119
    107120%TODO point out that the equation must be linear
    121(追記) (追記ここまで)
    122(追記) %TODO maybe to be extra clear, show a typical problem? (追記ここまで)
    108123
    109124\section{Terms, etc}
    … …
    123138 \end{itemize}
    124139\item Equations are kept normalised (GCD of coefficients $a_1 \cdots a_n$ is 1)
    140(追記) \end{itemize} (追記ここまで)
    141(追記) \end{frame} (追記ここまで)
    142(追記) (追記ここまで)
    143(追記) \begin{frame}[fragile] (追記ここまで)
    144(追記) \frametitle{$\land$ easy $\lor$ hard} (追記ここまで)
    145(追記) \begin{itemize} (追記ここまで)
    146(追記) \item All equations are joined by $\land$; $\lor$ effectively creates multiple equation-sets. (追記ここまで)
    147(追記) \item Integer division is not reversible (and requires rational numbers), so is avoided. (追記ここまで)
    148(追記) \item We are looking for integer solutions (追記ここまで)
    125149\end{itemize}
    126150\end{frame}
    … …
    218242\end{frame}
    219243
    244(追記) \begin{frame}[fragile] (追記ここまで)
    245(追記) \frametitle{Flow Chart} (追記ここまで)
    246(追記) \biggraph{Omega-Flowchart-M5} (追記ここまで)
    247(追記) \end{frame} (追記ここまで)
    248(追記) (追記ここまで)
    220249\begin{frame}
    221250\frametitle{Equality Solving Method}
    … …
    231260\end{frame}
    232261
    262(追記) %Some examples of modhat: (追記ここまで)
    263(追記) % (追記ここまで)
    264(追記) % 5 modhat 4: 1 (追記ここまで)
    265(追記) % 6 modhat 4: -2 (追記ここまで)
    266(追記) % 7 modhat 4: -1 (追記ここまで)
    267(追記) % 8 modhat 4: 0 (追記ここまで)
    268(追記) % 9 modhat 4: 1 (追記ここまで)
    269(追記) %10 modhat 4: -2 (追記ここまで)
    270(追記) (追記ここまで)
    271(追記) %define a blah b = floor(a/b + 1/2) (追記ここまで)
    272(追記) (追記ここまで)
    273(追記) % 5 blah 4: 1 (追記ここまで)
    274(追記) % 6 blah 4: 2 (追記ここまで)
    275(追記) % 7 blah 4: 2 (追記ここまで)
    276(追記) % 8 blah 4: 2 (追記ここまで)
    277(追記) % 9 blah 4: 2 (追記ここまで)
    278(追記) %10 blah 4: 3 (追記ここまで)
    279(追記) (追記ここまで)
    280(追記) \begin{frame}[fragile] (追記ここまで)
    281(追記) \frametitle{Final Flow Chart} (追記ここまで)
    282(追記) \biggraph{Omega-Flowchart-M4} (追記ここまで)
    283(追記) \end{frame} (追記ここまで)
    284(追記) (追記ここまで)
    233285\section{Inequalities}
    286(追記) (追記ここまで)
    287(追記) \subsection{Normalisation} (追記ここまで)
    234288
    235289%Section divider:
    … …
    289343\item Given an inequality in the conventional form: $\displaystyle\sum_{i=0}^n a_i x_i \geq 0$
    290344\item Normalise inequalities by finding $g,ドル the GCD of $a_1 \cdots a_n$
    345(追記) \item Divide $a_i$ ($i \geq 1$) by $g$ (追記ここまで)
    291346\item Set $a_0$ to $\lfloor a_0/g \rfloor$
    292347\end{itemize}
    … …
    294349}
    295350\end{frame}
    351(追記) (追記ここまで)
    352(追記) \begin{frame}[fragile] (追記ここまで)
    353(追記) \frametitle{Final Flow Chart} (追記ここまで)
    354(追記) \biggraph{Omega-Flowchart-M3} (追記ここまで)
    355(追記) \end{frame} (追記ここまで)
    356(追記) (追記ここまで)
    357(追記) \subsection{Eliminating Variables} (追記ここまで)
    296358
    297359\begin{frame}[fragile]
    … …
    339401Pick a variable (for illustration, $x_n$) and rephrase the set of inequalities 0ドル \leq \displaystyle\sum_{i=0}^n a_i x_i$ as:
    340402
    403(追記) %TODO this slide is quite dense and a little confusing. (追記ここまで)
    404(追記) %Would be really cool to animate the equations. Otherwise at least split i = 0 to n out into (追記ここまで)
    405(追記) % i = 0 to n - 1, plus the case for n (追記ここまで)
    406(追記) (追記ここまで)
    341407\begin{tabular}{cll}
    342408$a_n$ & Rephrase & Bound\\ \hline
    … …
    349415N.B. $a > 0,ドル $b > 0$
    350416
    417(追記) \end{frame} (追記ここまで)
    418(追記) (追記ここまで)
    419(追記) \begin{frame}[fragile] (追記ここまで)
    420(追記) \frametitle{Final Flow Chart} (追記ここまで)
    421(追記) \biggraph{Omega-Flowchart-M2} (追記ここまで)
    351422\end{frame}
    352423
    … …
    372443\end{frame}
    373444
    445(追記) \subsection{Shadows} (追記ここまで)
    446(追記) (追記ここまで)
    374447\begin{frame}[fragile]
    375448\frametitle{Bounding Pairs}
    … …
    388461\end{frame}
    389462
    390\begin{frame}(削除) <1-2> (削除ここまで)[fragile]
    463\begin{frame}(追記) (追記ここまで)[fragile]
    391464\frametitle{Shadows}
    392465\begin{itemize}
    … …
    510583\end{itemize}
    511584~\\
    512\begin{tabular}{ccc(削除) l (削除ここまで)}
    585\begin{tabular}{ccc(追記) c (追記ここまで)}
    513586$C_R = C_D$ & $\operatorname{hasIntSol}(C_R)$ & $\operatorname{hasIntSol}(C_D)$ & $\operatorname{hasIntSol}(C)$ \\
    514587\hline
    515588 \\
    516\tick & & & $ = \operatorname{hasIntSol}(C_R)$ \\
    517 & \cross & & \cross \\
    518 & \tick & \tick & \tick \\
    589%\tick & & & $ = \operatorname{hasIntSol}(C_R)$ \\
    590\tick & \tick & & \tick \\
    591\tick & \cross & & \cross \\
    592\cross & \cross & & \cross \\
    593\cross & \tick & \tick & \tick \\
    519594 \\
    520595 \hline
    … …
    524599\end{frame}
    525600
    601(追記) \begin{frame}[fragile] (追記ここまで)
    602(追記) \frametitle{Final Flow Chart} (追記ここまで)
    603(追記) \biggraph{Omega-Flowchart-M1} (追記ここまで)
    604(追記) \end{frame} (追記ここまで)
    605(追記) (追記ここまで)
    606(追記) \subsection{Last Resort} (追記ここまで)
    607(追記) (追記ここまで)
    608(追記) (追記ここまで)
    526609%TODO explain what to do in the difficult case!
    527610
    611(追記) (追記ここまで)
    612(追記) \begin{frame}[fragile] (追記ここまで)
    613(追記) \frametitle{Final Flow Chart} (追記ここまで)
    614(追記) \biggraph{Omega-Flowchart-Full} (追記ここまで)
    615(追記) \end{frame} (追記ここまで)
    528616
    529617%TODO represent the whole process as a flow chart to give a better idea of
    530618%how all these different cases fit together
    531619
    532(削除) \section{Tricky Parts} (削除ここまで)
    533(削除) (削除ここまで)
    534(削除) %TODO mention picking out i*j as a variable if possible (削除ここまで)
    535620
    536621\section{Code to Equations}
    537622
    538%TODO show code -> problem
    623\begin{frame}[fragile]
    624\frametitle{Replication}
    625\begin{itemize}
    626\item For parallel replication (e.g. 0 FOR 10), we introduce a ghost variable $i'$: 0ドル \leq i \leq i' - 1,ドル $i' \leq 9$
    627\item Effectively checking for any two arbitrary (non-equal) indices
    628\item Must check both ways!
    629 \begin{itemize}
    630 \item \lstinline|a[i] := a[i+1]| is `safe' for $i = i' + 1,ドル but not $i + 1 = i'$
    631 \end{itemize}
    632\end{itemize}
    633\end{frame}
    634
    635\begin{frame}
    636\frametitle{Flattening Expressions}
    637\begin{itemize}
    638\item Addition is left alone, subtraction is turned into addition.
    639\item Multiplied expressions are multiplied out.
    640\item Division is problematic if it doesn't cancel out.
    641\item Modulo is special \ldots
    642\end{itemize}
    643\end{frame}
    644
    645\begin{frame}[fragile]
    646\frametitle{Multiplied Variables}
    647\begin{itemize}
    648\item Any multiplied variables (e.g. \lstinline|i*j|) are treated as one (new) variable
    649 \begin{itemize}
    650 \item We can't express anything useful about them
    651 \end{itemize}
    652\item They often cancel out anyway:
    653\begin{lstlisting}
    654PAR i = 0 for 10
    655 scr[width*y + i] := 255
    656\end{lstlisting}
    657\item Set $\sigma = $ \lstinline|width*y|: $\sigma + i = \sigma + i' \implies i = i'$
    658\end{itemize}
    659\end{frame}
    660
    661\begin{frame}[fragile]
    662\frametitle{Modulo (REM) -- constant divisor}
    663\begin{itemize}
    664\item $x \operatorname{REM} y = x - \operatorname{sign}(x)|y| \lfloor \frac{|x|}{|y|} \rfloor$
    665\item Consider all three possibilities:
    666 \begin{itemize}
    667 \item $x = 0, x \operatorname{REM} y = 0$
    668 \item $m = -\lfloor \frac{|x|}{|y|} \rfloor: x \geq 1, x \operatorname{REM} y = x + m|y|, |y| - 1 \geq x + m|y| \geq 0, m \leq 0$
    669 \item $m = \lfloor \frac{|x|}{|y|} \rfloor: x \leq -1, x \operatorname{REM} y = x + m|y|, 1 - |y| \leq x + m|y| \leq 0, m \geq 0$
    670 \end{itemize}
    671 \note{Technically, the first case is subsumed by the latter two.
    672 But I expect that it will prove useful for efficiency reasons;
    673 you get two equalities, and those are easy for the Omega Test to
    674 deal with. The first problem should therefore be easy and quick.
    675 }
    676\item $y = 0$ implies division by zero
    677\item $y = \pm 1$ will almost certainly be unsafe ($\forall x: x \operatorname{REM} \pm 1 = 0$)
    678\end{itemize}
    679
    680\end{frame}
    681
    682\begin{frame}[fragile]
    683\frametitle{Modulo (REM) -- variable divisor}
    684\begin{itemize}
    685\item Previous solution, $x \operatorname{REM} y = x + m|y|$ doesn't work when $m$ and $y$ are both unknown
    686\item $x \operatorname{REM} y = x + a$ doesn't convey enough information
    687\item Consider positive $x$ and $y$
    688\item $a \leq 0, 0 \leq x + a \leq y - 1$ often still isn't enough.
    689 \begin{itemize}
    690 \item No upper bound on $y$ (unless we have further information)
    691 %TODO maybe explain this on some slides somewhere, briefly (the unbounded variables thing)
    692 \end{itemize}
    693\end{itemize}
    694\end{frame}
    695
    696\begin{frame}[fragile]
    697\frametitle{Modulo (REM) -- variable divisor}
    698\begin{itemize}
    699\item Instead of $a \leq 0,ドル consider two cases (recall: $a$ is a multiple of $y$):
    700 \begin{itemize}
    701 \item $a = 0$
    702 \item $a \leq -y$ ($\implies y \leq -a$)
    703 \end{itemize}
    704\item We can solve problems such as:
    705\end{itemize}
    706\begin{lstlisting}
    707[n]INT as: -- not valid occam (yet?)
    708PAR i = 0 FOR n
    709 as[(i + 1) REM n] := 42
    710\end{lstlisting}
    711\end{frame}
    712%TODO try Adam's problem from the last presentation
    713
    714%TODO we could probably cover all four x,y +- combinations:
    715%For negative y, use -y
    716%For negative x, change the sign of a (I think?)
    717%Even though four problems are generated, three are likely to be falsifiable quickly
    718
    719%replicated 0 FOR n. i + 1 REM n and j + 1 REM n, 0 <= i <= j - 1 <= n - 2
    720%
    721% Again, zero and negative options are inconsistent.
    722%
    723% Set a = some 0 or negative multiple of n, set b = some 0 or negative multiple of n. We know n is positive, so we know a <= 0, b <= 0
    724% We also know n - 1 >= i + 1 + a >= 0, n - 1 >= j + 1 + b >= 0
    725%
    726% i + 1 >= 1, j + 1 >= 1, i + 1 + a = j + 1 + b, n - 1 >= i + 1 + a >= 0, n - 1 >= j + 1 + b >= 0, a <= 0, b <= 0, 0 <= i <= j - 1 <= n - 2
    727% Trim:
    728% i + a = j + b, n - 2 >= i + a >= -1, n - 2 >= j + b >= -1, a <= 0, b <= 0, 0 <= i <= j - 1 <= n - 2
    729% Substitute i = j + b - a
    730% n - 2 >= j + b >= -1, a <= 0, b <= 0, 0 <= j + b - a <= j - 1 <= n - 2
    731% Separate out:
    732% n - 2 >= j + b
    733% j + b >= -1
    734% a <= 0
    735% b <= 0
    736% 0 <= j + b - a
    737% b <= a - 1
    738% j <= n - 1
    739% List out bounds for j:
    740% n - 2 - b >= j
    741% j >= -1 - b
    742% j >= a - b
    743% n -1 >= j
    744% Pair up bounds:
    745% n - 2 - b >= -1 - b, gives n >= 1
    746% n - 2 - b >= a - b, gives n >= 2 + a
    747% n - 1 >= -1 - b, gives n >= - b
    748% n -1 >= a - b, gives n >= 1 + a - b
    749%Also left over:
    750% a <= 0
    751% b <= 0
    752% b <= a - 1
    753% All variables have four bounds; n only has upper bound. Leave n (special case for algorithm!), eliminate a. Bounds are:
    754%
    755% 0 >= a
    756% a >= b + 1
    757% n - 2 >= a
    758% n -1 + b >= a
    759% Pair up bounds:
    760% 0 >= b + 1, gives -1 >= b
    761% n - 2 >= b + 1, gives n - 3 >= b
    762% n - 1 + b >= b + 1, gives n >= 2.
    763% Gather up everything (elim redundant 0 >= b, n >= 1):
    764% -1 >= b
    765% n >= b + 3
    766% n >= 2
    767% b >= -n
    768% So, bounds for b:
    769% -1 >= b
    770% n - 3 >= b
    771% b >= - n
    772% Pair up:
    773% -1 >= -n (gives n >= 1, redundant)
    774% n -3 >= -n, gives 2n >= 3, or n >= 2, redundant
    775% so overall, n >= 2 is the solution! Which we'd effectively already assumed...
    776% If we scan back up, we see n >= -b. We know b is a negative multiple of n. Take b' = -b/n.
    777% Therefore n >= b'n, where b' >= 0. Therefore b' is 1 or zero, b is zero or -n. Since n - 1 >= j + 1 + b >= 0
    778% either n -1 >= j + 1 >= 0 or n - 1 >= j + 1 - n >= 0. The latter gives j >= n -1 on the right, taken with j <= n - 1 gives j = n - 1.
    779%
    780
    781% Given the original problem (trimmed):
    782%
    783% i + a = j + b, n - 2 >= i + a >= -1, n - 2 >= j + b >= -1, a <= 0, b <= 0, 0 <= i <= j - 1 <= n - 2
    784%
    785% We know either a = 0, or a <= -n. Similarly, b = 0 or b <= -n. We can see that a = 0 , b = 0 gives i = j, but this will be inconsistent.
    786% Check if a = 0, b <= -n (gives i = j + b, subst):
    787% n - 2 >= j + b >= -1, b <= -n, 0 <= j + b <= j - 1 <= n - 2
    788% Arrange this into bounds for j:
    789% n - 2 - b >= j
    790% j >= - b
    791% n - 2 + 1 >= j
    792% Gives:
    793% n >= 2
    794% n >= 1 - b
    795% along with:
    796% b >= n
    797% -1 >= b
    798% Eliminate n:
    799% b >= 2
    800% 2b >= 1 (normalise: b >= 0)
    801% Along with:
    802% -1 > = b inconsistent!
    803
    804%
    805%
    806
    539807
    540808\section{Answers to Code}
    … …
    667935\end{tabular}
    668936
    669Error message: Unsafe when $-120 \leq 19z \leq -114,ドル 3ドルx + z = -63$ and $y = 5x + 3z$. Good luck!
    937\only<4>{Error message: Unsafe when $-120 \leq 19z \leq -114,ドル 3ドルx + z = -63$ and $y = 5x + 3z$. Good luck!}
    670938
    671939%TODO need to understand the omega test a little better to know all possible ways to improve this
    672940
    941(追記) %TODO the error will be more complex if there are fewer equalities (one); mainly inequalities (追記ここまで)
    942(追記) (追記ここまで)
    943(追記) %TODO If we only have a solution when there are 0 or 1 vars left, we can just set the 1 var (追記ここまで)
    944(追記) %equal to its remaining bound and then use the equality-substitution method. Just need to (追記ここまで)
    945(追記) %check this is possible for the exhaustive search method - I think so (追記ここまで)
    673946
    674947\end{frame}
    … …
    678951%TODO work through an example showing how to get the answer back to code (i.e. solution -> code)
    679952
    953(追記) \section{Future Work} (追記ここまで)
    954(追記) (追記ここまで)
    955(追記) \begin{frame}[fragile] (追記ここまで)
    956(追記) \frametitle{Future work -- reachability} (追記ここまで)
    957(追記) %Reachability (追記ここまで)
    958(追記) \begin{itemize} (追記ここまで)
    959(追記) \item Examining the indices directly is not always sufficient: (追記ここまで)
    960(追記) \end{itemize} (追記ここまで)
    961(追記) \begin{lstlisting} (追記ここまで)
    962(追記) SEQ i = 0 FOR 10 (追記ここまで)
    963(追記) n := i + 10 (追記ここまで)
    964(追記) a[n] := a[i] (追記ここまで)
    965(追記) \end{lstlisting} (追記ここまで)
    966(追記) \begin{itemize} (追記ここまで)
    967(追記) \item If we combine the Omega Test with reachability analysis we will be able to handle many more cases (追記ここまで)
    968(追記) \end{itemize} (追記ここまで)
    969(追記) \end{frame} (追記ここまで)
    970(追記) (追記ここまで)
    971(追記) \begin{frame}[fragile] (追記ここまで)
    972(追記) \frametitle{Future work -- advanced reachability} (追記ここまで)
    973(追記) We could use conditions in \lstinline|IF| and \lstinline|WHILE| as constraints: (追記ここまで)
    974(追記) \begin{lstlisting} (追記ここまで)
    975(追記) IF (追記ここまで)
    976(追記) n <= 0 (追記ここまで)
    977(追記) ... (追記ここまで)
    978(追記) TRUE (追記ここまで)
    979(追記) -- We can work out that: n > 0 (追記ここまで)
    980(追記) \end{lstlisting} (追記ここまで)
    981(追記) \end{frame} (追記ここまで)
    982(追記) (追記ここまで)
    983(追記) %TODO dead code removal? (追記ここまで)
    984(追記) (追記ここまで)
    985(追記) \begin{frame} (追記ここまで)
    986(追記) \frametitle{Future work -- optimising out checks} (追記ここまで)
    987(追記) \begin{itemize} (追記ここまで)
    988(追記) \item We can use the integer analysis to check if array indexes are always within bounds (追記ここまで)
    989(追記) \begin{itemize} (追記ここまで)
    990(追記) \item Hence we can remove run-time checks in places (追記ここまで)
    991(追記) \end{itemize} (追記ここまで)
    992(追記) \item Could even allow programmer to add a ``boundsafe'' annotation to the program, so that (追記ここまで)
    993(追記) an error will be given if all indexes are not definitely safe (追記ここまで)
    994(追記) \end{itemize} (追記ここまで)
    995(追記) \end{frame} (追記ここまで)
    996(追記) (追記ここまで)
    997(追記) \begin{frame} (追記ここまで)
    998(追記) \frametitle{Questions?} (追記ここまで)
    999(追記) \begin{itemize} (追記ここまで)
    1000(追記) %TODO put references here (the Pugh Omega Test paper, occam 2.1 manual, and maybe the Kessler paper (追記ここまで)
    1001(追記) \item Blah (追記ここまで)
    1002(追記) \end{itemize} (追記ここまで)
    1003(追記) \end{frame} (追記ここまで)
    6801004
    6811005\end{document}
Note: See TracChangeset for help on using the changeset viewer.

AltStyle によって変換されたページ (->オリジナル) /