summaryrefslogtreecommitdiffstats
path: root/formal
AgeCommit message (Expand)AuthorFilesLines
2023-07-02treewide: Remove ignored first parameter of origpub macrosPaul E. McKenney2-2/+2
2023-06-16formal: Clarify time RCU was added to the Linux kernelPaul E. McKenney1-2/+2
2023-05-27spinhint: Add clarifying step to QRCU by-hand proofPaul E. McKenney1-0/+5
2023-05-27formal: Fix referencesAlan Huang1-2/+2
2023-04-29Add acronyms of LKMM and KCSANAkira Yokosawa1-2/+2
2023-04-29formal/ppcmem: Use \qco{} as intendedAkira Yokosawa1-1/+1
2023-04-29formal/spinhint: Don't use \qco{} for long messageAkira Yokosawa1-1/+1
2023-04-09formal/ppcmem: Fix label name for Fail1:SeongJae Park1-1/+1
2023-04-09formal/ppcmem: s/powerpc/PowerPC/ on sentencesSeongJae Park1-1/+1
2023-04-09formal/ppcmem: Enclose example code snippets with \co{}SeongJae Park2-18/+18
2023-04-09formal/ppcmem: Add missed non-breakable spacesSeongJae Park1-2/+2
2023-04-09formal/ppcmem: Use \qco{} instead of ``\co{}''SeongJae Park1-5/+5
2023-04-09formal/ppcmem: Use uppercase 'S' for SpinSeongJae Park1-2/+2
2023-04-09formal/dyntickrcu: Use \qco{} instead of ``\co{}''SeongJae Park1-4/+4
2023-04-09formal/dyntickrcu: Quote 'trail' file consistentlySeongJae Park1-1/+1
2023-04-09formal/spinhint: Do not call 2013 paper as recentSeongJae Park1-1/+1
2023-04-09formal/spinhint: Enclose example code snippets with \co{}SeongJae Park1-4/+4
2023-04-09formal/spinhint: Use \qco{} instead of ``\co{}''SeongJae Park1-3/+3
2023-04-09formal/formal: Drop cppmem from 'Special-Purpose State-Space Search' section ...SeongJae Park1-1/+1
2023-01-04epigraph: Emphasize quoted text and book titlesAkira Yokosawa1-1/+1
2023-01-04Redefine \epigraph to avoid boilerplate \emph{}Akira Yokosawa6-8/+8
2022-08-08formal: Update list of Linux-kernel RCU changesPaul E. McKenney1-0/+10
2022-04-18index: Add indexing tags to memory barrier related termsAkira Yokosawa1-2/+2
2022-02-05formal/axiomatic: Tie in separation logic and spatial synchronizationPaul E. McKenney1-1/+3
2021-12-08treewide: Address potential widowing of headingsAkira Yokosawa1-11/+11
2021-11-02formal: Fix up per-Linux-kernel-version contentsPaul E. McKenney1-3/+4
2021-09-10formal: Fix another path of RCU-test-ratio.pdfAkira Yokosawa1-1/+1
2021-09-09formal: Move formal/data to CodeSamples/formal/dataAkira Yokosawa5-4503/+2
2021-08-31formal: Add commentary on Linux kernel v5.13 and v5.14Paul E. McKenney1-3/+14
2021-08-31formal: Update rcu-test data in Figure 12.4 (as of v5.14)Akira Yokosawa2-696/+754
2021-08-30index: Add index and acronym tags, take twoAkira Yokosawa6-12/+12
2021-08-10formal: Use \co{} for pan messages containing colonAkira Yokosawa1-2/+2
2021-08-10formal: Break and capitalize after colonAkira Yokosawa5-29/+42
2021-06-09treewide: Fix indents by white spacesAkira Yokosawa2-5/+5
2021-06-09treewide: Make end-of-sentence punctuation marks be at end-of-lineAkira Yokosawa1-2/+2
2021-06-09formal/dyntickrcu: Fix unintended paragraph breakAkira Yokosawa1-1/+1
2021-05-18formal: Employ \cref{} and its variantsAkira Yokosawa6-112/+112
2021-04-30formal: Add RCU changes for Linux kernel v5.12Paul E. McKenney1-0/+4
2021-04-30formal: Add v5.12 rcu-test data in Figure 12.4Akira Yokosawa2-545/+571
2021-04-27treewide: Fix space in front of \cite{}Akira Yokosawa1-2/+2
2021-04-27treewide: Make end-of-sentence periods be at end of linesAkira Yokosawa3-156/+187
2021-04-21index: Add index and acronym tags, take oneAkira Yokosawa2-4/+4
2021-04-11treewide: Remove explicit float positioning optionsAkira Yokosawa7-38/+38
2021-04-11treewide: Shrink floats for ebook-size buildAkira Yokosawa3-5/+12
2021-04-05acronym: Tag 'CAS' and its long/full formAkira Yokosawa1-1/+1
2021-04-04treewide: Mark non-end-of-sentence full-stop of 'vs.' as suchAkira Yokosawa1-1/+1
2021-03-19treewide: Address outdated commentaryPaul E. McKenney1-3/+3
2021-03-18treewide: Annotate sentence-ending fullstops as suchAkira Yokosawa4-12/+12
2021-03-15formal, together: Prevent intrusion of floats into non float snippetsAkira Yokosawa1-2/+2
2021-03-15formal: Add v5.11 rcu-test data in Figure 12.4Akira Yokosawa3-628/+654
2021-03-02treewide: url related updates, take twoAkira Yokosawa3-6/+6
2021-02-24formal: Normalize Taleb quotationPaul E. McKenney1-1/+1
2021-02-15formal: Add epigraph to last sectionPaul E. McKenney1-17/+19
2021-02-14formal: Updates and wordsmithingv2021.02.15aEdition.2-rc7Paul E. McKenney5-43/+58
2021-01-24treewide: Update to recent draft of the C++ standardPaul E. McKenney1-1/+1
2021-01-19formal: Update Figure 12.4 (refscale.c as test code)Akira Yokosawa2-20/+20
2021-01-19formal: Add commentary on changes in Linux-kernel RCUPaul E. McKenney1-0/+12
2021-01-19formal: Extend bar chart in Figure 12.4 up to Linux v5.10Akira Yokosawa3-1189/+1337
2020-11-24index: Add some more people index annotations in 'formal'Akira Yokosawa3-6/+7
2020-07-29formal: Retouch Table E.4Akira Yokosawa1-10/+16
2020-07-29Enhance qqz scheme for chapterwise QQZ answersAkira Yokosawa1-1/+3
2020-07-05formal: Add reference back to "two definitions"Paul E. McKenney1-2/+3
2020-06-15formal: Wordsmithing plus s/v2.6.16/v2.6.15/Paul E. McKenney1-11/+9
2020-06-15formal: Visualize Linux-kernel RCU test code ratioAkira Yokosawa5-98/+4266
2020-06-09formal: Add RCU use of formal verification to the choosing sectionPaul E. McKenney1-0/+2
2020-06-08formal: Add discussion of RCU's evolving test suitePaul E. McKenney1-7/+140
2020-06-07formal: Add a how-to-choose sectionPaul E. McKenney1-8/+113
2020-06-07formal: Update quick quiz on black hats and low-level codePaul E. McKenney1-0/+4
2020-03-26treewide: Use macros for consecutive quick quizzesAkira Yokosawa4-49/+62
2020-03-15treewide: Renew format of Quick Quiz macroAkira Yokosawa5-108/+108
2020-03-14formal/axiomatic: Move table env next to QQA's first paragraphAkira Yokosawa1-15/+16
2020-03-14Use 'Arm' as text trademark of Arm architectureAkira Yokosawa2-12/+12
2020-02-24Define and use \qtco{} to cover string containing breakable sequenceAkira Yokosawa1-1/+1
2020-01-31Rename environments 'linelabel' and 'lineref'Akira Yokosawa4-128/+128
2020-01-12Prevent section heading from orphanedAkira Yokosawa4-150/+141
2019-11-26treewide: Various typosStamatis Karnouskos2-3/+3
2019-11-24formal: Use \clnrefrange{}{} to refernece range of lines in snippetsAkira Yokosawa3-41/+41
2019-11-21typo correctionStamatis Karnouskos2-2/+2
2019-10-22treewide: Add '% mainfile:' tags in headers in sub .tex filesAkira Yokosawa7-1/+12
2019-10-06Define '\clnrefthro' for 'lines~m through~n'Akira Yokosawa1-1/+1
2019-10-06dyntickrcu: Apply 'cleveref' way of cross referenceAkira Yokosawa1-159/+132
2019-10-02ppcmem: Move final sentence of Answer to QQZ 12.27 to the nextAkira Yokosawa1-2/+2
2019-10-02ppcmem: Add Quick Quiz on lwsync in Listing 12.23Akira Yokosawa1-0/+29
2019-10-02ppcmem: Cite Git commit of PowerPC atomic_xxx_return fixAkira Yokosawa1-1/+2
2019-09-29ppcmem: Apply new scheme of code snippetsAkira Yokosawa1-94/+95
2019-09-29dyntickrcu: Fix trivial typoAkira Yokosawa1-1/+1
2019-04-21formal/dyntickrcu: Adjust context and fix typoAkira Yokosawa1-11/+20
2019-04-08formal/dyntickrcu: Cite git commits of dyntickrcu fixesAkira Yokosawa1-2/+2
2019-04-08formal/dyntickrcu: Fix the way to redefine VerbatimNAkira Yokosawa1-6/+2
2019-04-05formal/dyntickrcu: Mitigate ugliness of tall inline snippetsAkira Yokosawa1-29/+38
2019-04-05formal/dyntickrcu: Add nbspAkira Yokosawa1-2/+2
2019-04-05formal/spinhint: Tweak indent behind 'listing' environmentAkira Yokosawa1-0/+3
2019-04-05formal/dyntickrcu: Tweak indent behind 'listing' environmentAkira Yokosawa1-0/+7
2019-04-05formal/dyntickrcu: Remove '()' in state namesAkira Yokosawa1-6/+6
2019-04-05formal/dyntickrcu: Tweak appearanceAkira Yokosawa1-12/+13
2019-04-05treewide: Define and use \rt macro for '-rt'Akira Yokosawa1-3/+3
2019-04-05formal/dyntickrcu: Employ new scheme for code snippetsAkira Yokosawa1-778/+138
2019-04-05formal/dyntickrcu: Employ new scheme for inline snippetsAkira Yokosawa1-385/+381
2019-02-13formal/spinhint: Update QRCU patch prognosisPaul E. McKenney1-2/+1
2019-02-13formal/spinhint: Substitute ':formal:' for ':analysis:' in labelsAkira Yokosawa2-34/+34
2019-02-13formal/spinhint: Update memory usage in QRCU Spin summary tableAkira Yokosawa1-10/+10
2019-02-12formal/spinhint: Clarify hashtable sizes used in Tables 12.2 and 12.3Akira Yokosawa1-6/+8
2019-02-11formal/spinhint: WordsmithingPaul E. McKenney1-34/+34
2019-02-11formal/spinhint: Place footnote inside floating tableAkira Yokosawa1-6/+8
2019-02-11formal/spinhint: Add column of search depth in Table 12.2Akira Yokosawa1-13/+14
2019-02-11formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin runAkira Yokosawa1-4/+146
2019-02-02formal/spinhint: Update extrapolation for QRCU memory usagePaul E. McKenney1-1/+1
2019-02-02formal/spinhint: Use \co{...} rather than {\tt ...}Akira Yokosawa1-7/+7
2019-02-02formal/spinhint: Put footnote on header in tableAkira Yokosawa1-4/+6
2019-02-02formal/spinhint: Update tables of memory usage of SpinAkira Yokosawa1-25/+39
2019-02-02formal/spinhint: Update output lists of spinAkira Yokosawa1-117/+10
2019-02-02formal/spinhint: Employ new scheme for code snippetAkira Yokosawa1-483/+198
2019-01-16formal: Add LKMM citationsPaul E. McKenney1-2/+3
2019-01-15formal: Include performance results for locking verificationPaul E. McKenney1-2/+75
2018-12-02formal: Add C-Lock1 and C-Lock2 as proper litmus tests under CodeSamplesAkira Yokosawa1-53/+7
2018-11-19formal/axiomatic: Add missed parentheses for 'WRITE_ONCE()'SeongJae Park1-1/+1
2018-11-19formal/axiomatic: Fix a typo: s/Figure/ListingSeongJae Park1-1/+1
2018-10-31formal: Miscellaneous fixes and updatesPaul E. McKenney2-3/+22
2018-10-31formal/axiomatic: Fill in missing ')'Akira Yokosawa1-1/+1
2018-10-31formal/axiomatic: Convert snippets of IRIW tests to new schemeAkira Yokosawa1-52/+49
2018-10-31formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmusAkira Yokosawa1-55/+7
2018-10-31formal/axiomatic: Import snippet from C-RCU-remove.litmusAkira Yokosawa1-32/+4
2018-10-30formal/axiomatic: Add example locking litmus testsPaul E. McKenney1-2/+96
2018-10-29formal/axiomatic: Add example RCU litmus testsPaul E. McKenney1-1/+236
2018-10-28formal/ppcmem: Fix labels by removing extraneous "sec:"Paul E. McKenney1-11/+11
2018-09-01formal: Add section-level epigraphsPaul E. McKenney6-3/+25
2018-05-21Forward-reference the formal-regression sectionPaul E. McKenney1-0/+5
2018-04-06future/formalregress: Move formal regression testing to future chapterPaul E. McKenney2-603/+0
2018-04-06formal/sat: Add DATE'18 citationPaul E. McKenney1-1/+1
2018-02-15formal: Hardware also has empirical specificationsPaul E. McKenney1-1/+4
2018-02-15formal: Add figures for CBMC and Nidhugg processing flowPaul E. McKenney4-2/+1154
2017-12-12Fix typo: s/Curiosty Rover/Curiosity Rover/SeongJae Park1-1/+1
2017-12-09formal: Emphasize bug injection as formal-tool testing techniquePaul E. McKenney1-0/+7
2017-12-06formal/sat: Sharpen up discussion of bug injectionPaul E. McKenney1-5/+9
2017-11-18formal: Plural section name for "stateless model checker"Paul E. McKenney2-3/+3
2017-11-05formal/regression: Restore escape to '%' symbolAkira Yokosawa1-1/+1
2017-11-03formal: Fix spelling error s/postives/positives/Paul E. McKenney1-1/+1
2017-11-03formal, memorder: Fix typo and adjust spacingAkira Yokosawa2-4/+4
2017-11-03formal: Complete verification-limitations thought in QQ12.33Paul E. McKenney1-1/+3
2017-11-02formal: Update bug-injection rate and clarify reasoningPaul E. McKenney1-12/+52
2017-10-31memorder: Remove PA-RISCPaul E. McKenney1-1/+1
2017-10-30formal/regression: Add Mars rover example for PromelaPaul E. McKenney1-1/+4
2017-10-30formal/regression: Update from self-reviewPaul E. McKenney1-7/+32
2017-10-30debugging,formal: Update for increased Linux kernel usagePaul E. McKenney1-10/+23
2017-10-30formal/regression: Fix typoAkira Yokosawa1-5/+5
2017-10-29formal: Add paths and clean up tablePaul E. McKenney1-6/+11
2017-10-29formal: Fix "Scorcard" typo and add that section to roadmapPaul E. McKenney1-3/+5
2017-10-29formal/regression: Tweak table format and indent in listingAkira Yokosawa1-64/+69
2017-10-28formal: Add Nidhugg and regression requirementsPaul E. McKenney2-0/+518
2017-10-28formal: Add section on stateless model checkersPaul E. McKenney2-0/+31
2017-10-22Update tables using booktabs and alternate-row coloring schemeAkira Yokosawa1-35/+33
2017-10-17formal: Add recent cbmc/SAT progressPaul E. McKenney1-4/+27
2017-10-12Convert code snippets to 'listing' env (datastruct, debugging, formal)Akira Yokosawa4-130/+130
2017-10-05treewide: Use "IRQ" instead of "irq" used as abbreviationAkira Yokosawa1-25/+25
2017-10-05treewide: Call GNU C compiler as "GCC"Akira Yokosawa1-1/+1
2017-10-05treewide: Insert narrow space in front of percent symbolAkira Yokosawa2-2/+2
2017-06-24treewide: Add narrow spaces before non-SI unit symbolsAkira Yokosawa2-5/+5
2017-04-04Make Formal-Verification chapter label match conventionPaul E. McKenney2-3/+3
2017-03-14formal/spinhint: Reference by Figure labelsAkira Yokosawa1-1/+3
2017-03-14formal/spinhint: Adjust option of enumerate listAkira Yokosawa1-4/+4
2017-03-14formal/spinhint: Fix typoAkira Yokosawa1-2/+2
2017-03-09Fill in details of QRCU-like benchmarkPaul E. McKenney1-11/+49
2017-03-09formal: Convert to 'description'Akira Yokosawa2-13/+13
2017-01-04Revert "formal/dyntickrcu: Adjust font size of sample code"Akira Yokosawa1-1/+1
2016-11-16treewide: Adjust labeling of 'formal'Akira Yokosawa1-1/+1
2016-11-16formal: Promote \OriginallyPublieshed macro to ChapterAkira Yokosawa1-1/+1
2016-10-26formal: Replace 'article' with 'section'Akira Yokosawa1-1/+1
2016-09-27formal/dyntickrcu: Adjust font size of sample codeSeongJae Park1-1/+1
2016-09-27formal/ppcmem: Polish a sentence by removing unnecessary conjunctionSeongJae Park1-1/+1
2016-09-27formal/ppcmem: Substitute `paper` with `chapter`SeongJae Park1-2/+2
2016-09-27formal/ppcmem: Use P0 instead of thread 1SeongJae Park1-1/+1
2016-09-27formal/ppcmem: Use \co{} for instruction quotationSeongJae Park1-1/+1
2016-09-27formal/ppcmem: Fix typo for \co{}SeongJae Park1-1/+1
2016-09-27formal/dyntickrcu: Fix wrong function name quotationSeongJae Park1-1/+1
2016-09-27formal/dyntickrcu: Fix wrong line number quotationSeongJae Park1-3/+3
2016-09-27formal/dyntickrcu: Fix typosSeongJae Park1-3/+3
2016-09-27formal/dyntickrcu: Append `()` to function name quotationsSeongJae Park1-13/+13
2016-09-27formal/dyntickrcu: Add missing NBSPsSeongJae Park1-32/+32
2016-09-27formal/spinhint: Reference figureSeongJae Park1-1/+1
2016-09-27formal/spinhint: Use \co{} for variable quotation consistentlySeongJae Park1-1/+1
2016-09-27formal/spinhint: Use \path{} for file name quotationSeongJae Park1-1/+1
2016-09-27formal/spinhint: Fix typosSeongJae Park1-2/+2
2016-09-27formal/spinhint: Add missing NBSPsSeongJae Park1-4/+4
2016-09-19epigraph: Use \epigraphhead{}Akira Yokosawa1-2/+2
2016-09-14treewide: Enclose 'verbbox' within 'figure'Akira Yokosawa4-29/+29
2016-08-25Add a few more non-breaking spaces in line numbersPaul E. McKenney1-29/+29
2016-08-25treewide: Use nbsp after 'Lines' and 'lines'Akira Yokosawa2-29/+29
2016-08-11Update and create .gitignore filesAkira Yokosawa1-0/+1
2016-08-11Remove .eps files whose sources are .fig filesAkira Yokosawa1-4120/+0
2016-08-08Add \nbco{} command for code snippet without line breakAkira Yokosawa1-1/+1
2016-08-08formal/ppcmem: Avoid break-line after 'lines' in sourceAkira Yokosawa1-2/+3
2016-07-26Use unspaced em dashes consistentlyAkira Yokosawa1-1/+1
2016-07-25Use UK style punctuation orderAkira Yokosawa2-2/+2
2016-07-19formal: Trivial typo fixesAkira Yokosawa1-2/+2
2016-07-17Update formal-verification conclusionPaul E. McKenney1-9/+10
2016-07-09Tweak sizes and positions of Tables and FiguresAkira Yokosawa2-3/+5
2016-07-09Use \centering instead of center environment (part 3)Akira Yokosawa2-6/+3
2016-07-03Apply SPDX license identifiers to unambiguous filesPaul E. McKenney2-0/+2
2016-07-02formal: Use \path command for path namesAkira Yokosawa3-24/+24
2016-07-02formal: Centering figures of verbatim code examplesAkira Yokosawa4-89/+145
generated by cgit 1.2.3-korg (git 2.39.0) at 2024-05-17 08:56:00 +0000