​

Software (in-)Correctness Analysis

Lecture-2

​

Ganesh Gopalakrishnan

Summary of Lec-1

• Bugs when humans get complacent (lose their ability to distrust things)
• Keystrokes entered in a calculator are wrong, and yet blindly believe what the calculator gives
• Or when companies hide information - as a matter of practical difficulties or deliberately
• Documentation is expensive and official documentations not agreeing with real system are even more trouble
• CS folks need to know how much to trust companies
• In today's climate this is inevitable
• Google Doc so widely used, and Apple M1 chips compute things for us
• Does the society simply trust companies, hoping for unlimited altruism?
• Experience shows that having "good-natured vigilantes is good for all"
• Our ASPLOS'15 paper: https://dl.acm.org/doi/10.1145/2775054.2694391
• Products from companies are widely different
• No two embedded GPUs agree in terms of their weak-memory semantics
• https://gpuharbor.ucsc.edu/
• Yet, society will use such mobile GPUs on phones and IoT soon
• Ask me about a concept building in France that is fully computer-controlled
• Or when behaviors are non-intuitive
• Floating-point, concurrency, weak memory models, complex control-flows, too many cases
• Or when the interfaces are too broad
• No abstraction for the interfaces exposed

​

Systems ARE getting ultra-complex

​

Software bugs are a huge drain on the national economy (not to speak about the security consequences which are graver)

​

Formal methods to analyze software are hugely important for companies (it is widely recognized to be a good source of internships and employments for grad students)

Additional thoughts on projects

• You will earn a lot of respect if you "get real" and "get physical"
• I have some cool hardware
• BBC Micro V2, Rock-5 Model-B computer, NVIDIA Jetson Xavier, Raspberry Pi
• I can buy more
• If you do the design of something on it (e.g. object-tracking etc)
• Maybe even as part of another class (e.g. Prof. Hall's GPU class)
• then you can verify those designs in my class!
• There are ultra-cool projects that are turning "Apple's head" and others
• https://cs.stanford.edu/people/trippel/ has projects on test-generation for comp arch
• https://allisonius.github.io/research/ has projects on test-case generation
• https://github.com/NVlabs/litmustestgen is an NVIDIA-research tool for test generation
• Test-generation is a great way to package formal methods
• "You are not hitting someone on their knuckle saying - bug!"
• You are instead giving them something free - tests!
• Same idea in QuickCheck : https://en.wikipedia.org/wiki/QuickCheck
• and QuickChick : https://github.com/QuickChick/QuickChick for coq
• Yes, test-generation for theorem-provers !! Why not?
• esp with Neural Theorem-proving, we need training data!

​

​

What to study first, and what background needed?

• We will study protocol modeling
• Using the Promela language
• which uses the SPIN model-checker
• What is a model-checker in general?
• Here it is, generically
• System |= Property
• For example
• TrigLibrary |= sin^2(theta)+cos^2(theta) = 1
• System "satisfies" Property ( |= is "satisfies")
• We will do this
• Elevator |= (Henceforth (ButtonPush => Eventually ElevatorArrive))
• Elevator |= [] (ButtonPush => <> ElevatorArrive) ← this is a temporal-logic property
• This is achieved as follows
• We need the language of the Elevator (Elevator == Buchi Automaton) ← assume B\"{u}chi
• All the behavioral-traces it generates
• We need the language of the property (Property also == Buchi Automaton)
• The set of traces that model the temporal-logic property
• Lang(System) contained-in Lang(Property)
• which is equivalent to
• Lang(System) INTERSECT Complement(Lang(Property)) == empty-set

Do you agree? Questions? (5-min pause)

​

Where did this line of thought come from?

• If I don't tell you the history a bit, you'll be robbed of all these facts
• My contribution for the resources I've enjoyed over 4 decades of grad studies + work
• Alan Turing, 1940s
• Proved a program by hand!
• First program proof
• 1960's
• Dijkstra pretty much started
• with concurrency verification !!!!!!! ← with multicore, IoT, self-driving cars, importance very high
• Dijkstra knew concurrency was hard
• Advocated that one write non-deterministic loops
• do :: guard1 -> action1 :: guard2 -> action2 od
• Smooth specification that does not preordain an irrelevant order
• for (i=0; i<53; i++) { who cares? i could have gone from 52 to 0 also !! }
• Aside: if you can take a loop like this, parallelize it, and run it backward OK, then this loop has no data races! :-)
• forget this if you find this confusing
• Floyd, Hoare
• Sequential program verification
• Like pushing a car uphill ?
• That is what Alan Perlis, Lipton and DeMillo said
• "Social Processes…"

History of Temporal Logic (brief)

• Amir Pnueli, 1978, Turing Award, alas not with us
• Told me this when he hosted my visit at Weizmann Institute in Israel, year 2000 !!
• Israeli planes flying overhead, I was chased down by a security guard.. (for badge-check) – fun days
• Saw Israel's first supercomputer - Weizak - nice story here (later)
• Sought logic for concurrency
• Someone gave him a book
• Closing cover of book had "other books from publisher"
• Modal Logic
• Aha Temporal Logic => …………. => Turing Award!
• Manna and Pnueli
• Temporal proofs by hand
• Now pushing temporal-logic-proof-car uphill :-(
• Lamport also did major work in TL
• Enter Clarke, Emerson, Sifakis
• "Enhance success by dumbing-down expectations" (a good message for your PhD)
• Let's model-check not prove
• Wrote first model-checker
• For Computational-Tree Logic (relevant for aspect-oriented programming)
• Now car climbs hill on its own, but slowly !!! :-)

Birth / rediscovery of BDDs (birth, as canonicity was emph.)

• Enter Randy Bryant
• Doing Fault Simulation (told me at a nice conference banquet!)
• Needed Efficient Boolean Representation
• Truth-tables suck !! Always EXP sized !!

Do you see the ugliness ?

​

"draw a truth-table for the MSB when adding two 64-bit numbers"

​

"turn in the assignment in a week" (extension - a year ->...)

​

Doable?

BDD

• Enter Randy Bryant
• Doing Fault Simulation
• Needed Efficient Boolean Representation
• Truth-tables suck !! Always EXP sized !!

Do you see the ugliness ?

​

"draw a truth-table for the MSB when adding two 64-bit numbers"

​

"turn in the assignment in a week" (extension - a year ->...)

​

Doable?

​

"The ability to see ugliness is the beginning of wisdom"

Where did this line of thought come from?

• Bryant showed we can build a linearly-sized data structure (often) for Boolean functions
• BDD
• Did not write in his initial paper that BDD are minimal DFA also
• You will see it in Asg-1
• BDDs powered the first wave of formal verification
• BDDs are wonderful and are getting re-discovered
• This is why one never passes up fun theory
• Comes in handy even after "spent"
• i.e. BDDs were golden till about 1998
• Then Boolean SAT sped up
• BDD sat in the backseat as a neglected child…
• Now coming back in force (not exactly a SAT tool - hence)
• Donald Knuth has spent 140 pages in his newest algo book on BDD
• Calls BDDs "one of the most interesting data structure of the past 25 years"
• BDD revival
• https://web.cs.ucla.edu/~guyvdb/papers/HoltzenOOPSLA20.pdf (probabilistic programming)
• CFLOBDDs
• https://arxiv.org/abs/2211.06818 ← invented 22 years ago
• There is even a patent for GrammaTech
• Now suddenly hot for quantum circuit simulation
• Looks full of matrices and tensors
• Need to see if we can "rip this out and use for tensor networks ?!?! " ← will as Thanson !!!

Connection with decision-trees?

• Some similarities
• many differences
• ask me

How did BDDs power model-checking?

• Bryant showed we can build a linearly-sized data structure (often) for Boolean functions
• Ken McMillan in CMU as grad-student during this time (1987ish)
• Invented algorithm for CTL model-checking using BDD (in his first few semesters!)
• Now temporal-logic car goes uphill on its own reasonably fast!
• Many say Ken McMillan ought to have shared the Turing Award for model-checking awarded to Clarke, Emerson and Sifakis
• I agree with this sentiment ("being junior and too nice → awards overlooked?")
• Ken McMillan's algorithm is called Symbolic Model Checking
• Daniel Jackson of MIT writes
• "Symbolic Model Checking make formal methods respectable"
• We probably will write (thru an assignment) this model-checker
• teaches you
• recursion
• (never get enough)
• least and greatest fixpoints
• (ditto)
• logic and existential quantification
• (ditto)

How did Buchi automata come about? What other model- checkers?

• Linear-time temporal logic was the first proposed (Pnueli)
• Vardi, Wolper, Yannakakis studied it extensively
• Automaton-Logic Connection!
• LTL formulae have Buchi Automata that include all and only the same satisfying traces
• Stay tuned
• LTL vs. CTL wars
• went on for 20 years till all agree it is pointless
• Industry uses both or a mixture
• Gerard Holzmann
• Early pioneer in model-checking at Bell Labs
• Infused above ideas
• Worked on Promela (language) and SPIN (tool)
• nearly 40 years of steady maintenance
• Perhaps the world's most renowned model-checker
• Versatile in the right hands
• You can learn it and use it life-long whenever you are stuck modeling a protocol
• David Dill
• Worked on Dash and Flash coherence protocols (Stanford, early 90s or maybe late 80s)
• Needed a different notation to capture symmetry and "rule-sets"
• Murphi
• Dave told me this was intended to be thrown away soon
• Never happened – Murphi and its derivatives Rumur and ROMP are alive

What is a Buchi Automaton? Difference with DFA?

• Buchi automata are finite automata that accept ONLY infinite words
• yes you heard it right
• eh?
• something like a ^ infinity or a^omega
• When you must harbor an a^omega path in any finite-state machine, how does such a path ALWAYS look?
• Think Pigeon-hole Principle and Pumping Lemma…

What is a Buchi Automaton? Difference with DFA?

• Buchi automata are finite automata that accept ONLY infinite words
• yes you heard it right
• eh?
• something like a ^ infinity or a^omega
• When you must harbor an a^omega path in any finite-state machine, how does such a path ALWAYS look?
• Think Pigeon-hole Principle and Pumping Lemma…
• Infinite paths are cycles in a finite-state graph !! No other choice!

Agree ?

What is a Buchi Automaton? Difference with DFA?

• Buchi automata are finite automata that accept ONLY infinite words
• yes you heard it right
• eh?
• something like a ^ infinity or a^omega
• When you must harbor an a^omega path in any finite-state machine, how does such a path ALWAYS look?
• Think Pigeon-hole Principle and Pumping Lemma…
• Infinite paths are cycles in a finite-state graph !! No other choice!
• To quickly understand the difference, we will look at the "same picture" (finite-state diagram) first as a DFA and then as a DBA
• Just change the color of your eye-glass lens!
• Violet-lens ⇒ DFA
• Blue-lens ⇒ DBA

What is a Buchi Automaton?

Difference with DFA?

• language of DFA1 as an RE?
• DFA2?

​

​

​

Guess language of DBA1,2 if I tell you that only those infinite strings exist

that touch an accepting state (double-circle) infinitely

​

write such strings as (small-string) raised to omega

​

what is the small string?

​

Think !!

What is a Buchi Automaton?

Difference with DFA?

• DFA1 has a(ba)*
• DFA2 has (ab)*
• DBA1 and DBA2 have the same language
• which is (ab)^omega

Back to Slide 4

• We need practice wrt "A contained-in B" like situations!
• Lang(System) contained-in Lang(Property)
• which is equivalent to
• Lang(System) INTERSECT Complement(Lang(Property)) == empty-set
• We need to be doing this often
• Later , the SPIN tool will do it for you
• setA containedIn? setB

​

turns into

​

BA1 containedIn BA2

​

BA1 intersect complement(BA2) is empty

​

You need practice complementing and intersecting machines

​

Let's get that practice using ordinary DFA first → next week we will do it for BA

Intermission

This Lecture – after Intermission!

• Classical automata (DFA, NFA) and regular expressions
• How to verify constructions – not merely test them
• Diff two machines to obtain a third machine
• How to represent Boolean functions compactly
• BDDs
• How to read paths in a BDD as CNF or DNF
• BDDs can be viewed as slightly optimized minimal DFA for the set of satisfying instances under consideration
• Let's run the two notebooks of Asg1 and Asg2
• I have a ton of lecture slides and videos from CS 3100
• Ask T.M. Tanmay to give them to you – or post them to this Canvas…
• or even somehow get the recordings from CS 3100 come into Media Gallery

​

• Automaton Colab "Jove" notebook
1. https://drive.google.com/file/d/1uVWMkMq0-ZSsEkkEnXXAkH78q6kAnP6c/view?usp=share_link

​

• BDD Notebook
• https://drive.google.com/file/d/1rONoPhaG44z_Vi_kd08m1ED5mJGW3y8-/view?usp=share_link

​

This Lecture's Summary

• DFA are powerful
• Can be used to realize lexers, understand BDDs, and also represent the truth of Presburger arithmetic
• Studying DFA design can be a good exercise in specification and verification
• We will then study how to model problems using BDD
• And understand CNF/DNF
• This prepares us well for Buchi automata and
• NBA - nondeterministic Buchi automata
• DBA - deterministic Buchi automata
• For some NBA there are no DBA
• NBA correspond with (and are obtainable from) Linear-time Temporal Logic assertions
• Will do a live demo and record today's lecture

READINGS for Lec-3

• First several chapters of Ben-Ari's book

​

EXPECT THESE this weekend

​

• Quiz-1 reviewing this week

​

BE DOING THESE READINGS

​

• Ben-Ari's book chapters (however much you can read will help – say at least two chapters)
• Read pertaining to background + projects

​