diff options
| author | SeongJae Park <sj38.park@gmail.com> | 2023-12-02 09:26:13 -0800 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-12-02 11:25:42 -0800 |
| commit | 4e380fbb497669a0c1dbc133581969b6fe0f1e16 (patch) | |
| tree | 5f77aa7eedd0030d40d02ba63d08205645fb9d01 | |
| parent | 2784f34c91968bd6521bdf05e89368821acd6d41 (diff) | |
| download | perfbook-4e380fbb497669a0c1dbc133581969b6fe0f1e16.tar.gz | |
future/formalregress: Use \co{} for spin
formalregress.tex is using \co{} for spin in most cases. Use it always
for better consistency.
Signed-off-by: SeongJae Park <sj38.park@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
| -rw-r--r-- | future/formalregress.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/future/formalregress.tex b/future/formalregress.tex index a50df4ad..b1a39b29 100644 --- a/future/formalregress.tex +++ b/future/formalregress.tex @@ -155,7 +155,7 @@ testing, which is in fact the topic of this section. It is critically important that formal-verification tools correctly model their environment. One all-too-common omission is the memory model, where a great -many formal-verification tools, including Promela/spin, are +many formal-verification tools, including Promela/\co{spin}, are restricted to \IXh{sequential}{consistency}. The QRCU experience related in \cref{sec:formal:Is QRCU Really Correct?} @@ -359,7 +359,7 @@ What is needed is a tool that gives at least \emph{some} information as to where the bug is located and the nature of that bug. The \co{cbmc} output includes a traceback mapping back to the source -code, similar to Promela/spin's, as does Nidhugg. +code, similar to Promela/\co{spin}'s, as does Nidhugg. Of course, these tracebacks can be quite long, and analyzing them can be quite tedious. However, doing so is usually quite a bit faster |