​

Software (in-)Correctness Analysis

CS 5110 / 6110

​

we'll use 6110 always

(moved all students from 5110 here)

​

Ganesh Gopalakrishnan

Overview: Want free, humane, and green help!

• There is nothing like humane free help
• Prefer animals over people (we evolved since the dark ages)
• Prefer machines over animals (we evolved with the Steam Engine but lots of CO2)
• Prefer green machines that self-destruct after use and nourish the earth (yet to happen)
• Humane free help (not green yet) invades our lives
• Spreadsheet
• Chatgpt – an AI agent that "writes code for you"
• (and almost wipes your runny nose…)
• GPS

Overview

​

• Humane free help (not green yet) invades our lives
• Spreadsheet
• Chatgpt
• GPS
• Humans de-train themselves
• We are cocksure that we can check Chatgpt results
• We do this OK for a while
• Then we forget basic math and basic everything
• Till we get so stupid that we follow the machine
• Person in Germany drove car into a port-a-potty because the GPS told him so
• Observation
• Bugs happen when humans love free help so much that they lose the instincts to distrust

Overview

​

• Bugs also happen because companies hide details
• Linux laptops suck because manufacturers don't reveal the power settings
• Windows feels better
• (Un)Holy alliance of Intel and Microsoft
• Companies are not evil
• But they do things to ward-off competition
• This hides stuff
• This prevents the public eye from debugging
• If you are Apple, you then hire the world's talent to be in-house
• Intel did not reveal the x86 memory model
• Lots of vigilantes needed to pry open the doors
• Sewell and co
• Nvidia plays cat and mouse (everyone does ; Nvidia not unique)
• Can't pry the SASS semantics from them

​

Overview

​

• Bugs also happen because people can't communicate enough
• I often visit companies - Intel - and tell what one division is doing to another
• That is news!
• The Intel FDIV bug happened because of this
• Viktor Konrad told me that they had wonderful FDIV tests
• But the division making the SRT division algorithm wasn't provided this info

Overview

​

• Bugs happen when intuition fails
• for (i = 0.0; i < 1.0; i += 0.1) printf("in loop")
• Prints "in loop" 10 times when running FP32
• prints 11 times when running FP64
• It keeps dancing 10, 11, 10, 11 … till you allocate FP128 (roughly)
• Then it is always 10
• all the concurrency bugs are because the brain can't grok
• data races
• cache coherence
• tricky non-blocking queues
• The volume of code these critical constructions occupy is not much
• Like ball-bearings
• Very small fraction of a ship
• Yet, one grain of sand in one critical bearing → ship can sink
• "Bugs are in the interstices" – Prof. John Baugh
• Interstices == (roughly) the armpits

Overview

​

• Bugs don't happen that much in "squeaky clean code"
• Nice loop-based matrix-multiplication
• Of course look at corner-cases (interstices or pits)
• Loop beginning
• Loop end
• Spot-check in the middle
• "Engineer's induction" !!

Overview

​

• Moral
• Write squeaky-clean code almost always
• Interstices are unavoidable
• When you push on performance
• Then you have to "bare it all"
• You lose abstraction boundaries
• No time to invent new abstractions
• "Gotta ship"
• Thus you live with broken abstractions
• Soon the academics invent nice abstractions
• The interstices have formal semantics
• But then more performance needed
• More interstices open up
• THE SAGA CONTINUES

Summary

​

• When we want free humane and green help to get things done fast
• We keep opening up new interstices
• We invent ways to close them

​

​

That is the topic of this class !!

​

​

​

​

(this class == how to close the pits?)

Now we need free help elsewhere!

​

• So now we are in the second layer
• Code gets free work ⇒ Code needs to be debugged ⇒ that is a lot of work ⇒ need free help

This class == Automata + logic for free debugging help!

​

• WE NEED TO CLEAR THE AIR and our minds
• Put on a game-face
• Loose-speak is bad
• Loose lips sink chips (thanks Subra / Gary)

This class == Automata + logic for free debugging help!

​

• Rigor helps
• Rigor helps us invent scalable debugging methods
• Fast checking of automata
• Humans are indirectly getting smarter
• Nobody tell them - hush!
• Fast checking using logic
• Lots of speed via mocking NP-completeness on its face
• Soon we say rigor unnecessary
• Humans don't often acknowledge all the crutches that got them to grow
• baby food, diapers, …
• Think they were Lebron James's from birth
• They invent fuzzing
• Now write papers such as this
• https://wcventure.github.io/FuzzingPaper/Paper/FSE19_JFI.pdf
• Heehee no stinking theory

​

Pay obeisance to theory first; then hack!

​

• You gotta pay respects
• Then spit on palms and hack
• Else
• when you need new interstices to be filled
• You would have de-trained yourselves from inventing the next abstraction
• Besides
• theory helps you look smart
• Helps you jut your jaws forward and walk around
• Dude, this browser uses FHE – your's reeks
• Theory is now window-dressing
• This bridge was designed using partial differential equations !!
• This browser uses the theory of Micali and Goldwasser
• Oops no
• Soon you get decertified
• You gotta provide measurable security

Pay obeisance to theory first; then hack!

​

• Security through obscurity is bad
• Name-dropping formal (as if holy water) is equally bad
• Formal can be gum you chew and spit
• At least acknowledge that your jaws got the work-out

But formal is becoming bottomline!

​

• Can't ship chips w/o it
• you can, but the quality will tank
• blue-screen, vulnerabilities
• Remember the deep formal in-house talent so you can avoid exposing API
• True even for SW
• projects where they are preferring
• Formal, careful, take more time to debug

over

• Informal, ship quickly, suffer pain of fixes
• Heard it from designer of advanced file systems
• Formal is jobs
• If you do the right formal, you'll get jobs
• Right formal could mean (guessing)
• Making LLVM robust
• Fuzzing anything
• Breaking anything + finding fixes
• People who do formal for systems better often are better at systems

Three-layered process?

​

• Test
• remove shallow bugs
• Fuzz
• next level bugs
• Model-check or SMT
• more bugs and for practical purposes a stopping-point
• SW model-checking
• more bugs for pithy code
• Theorem-prove
• if done right and meaningfully, it is great
• Helps document better
• Specs can transcend people/projects
• Specs turn into tests
• Good loop to have

​

​

Big elephants coming our way

​

• ML will be our boss
• Hard to define what "correct" means
• 90% test accuracy may not mean "the right 90%"
• How do we prefer confusing an arm for a leg

over

• An arm for a ship
• Tough spot we are on
• HPC was here too
• No fuzzing tools for HPC
• It largely is experimental machinery
• If you stray outside Physics you compute nonsense
• But we have to have heavy hammers that fuzz HPC and ML
• Lots of exciting important research
• Collaborator of mine is developing modern power systems
• She simulates Ax = b
• Matrix A is almost singular yet meaningful
• Every solver NaNs out!
• HELP!!
• Projects on meaningful FV for ML encouraged
• What I've seen is looking under the light (small problems)
• Not looking where the bugs are in big systems (gotta go empirical first)
• Data movement is coming our way
• Will ship compressed data across chiplets
• Decompress and compute
• OK?

​

Syllabus (roughly)

​

• Basics of automata and logic
• My book on Canvas
• Automata and Computability : a programmer's perspective
• Promela and SPIN
• Ben-Ari
• KLEE and CBMC
• symbolic execution
• practice loop invariants but check first via KLEE
• Then CSeq
• Hey now concurrency!
• Map things in Promela to things in PThreads
• Verify again using CSeq

Syllabus (roughly)

​

• Parallel random-walk
• Murphi and ROMP
• Swarm-testing in SPIN too?
• SAT and DPLL
• and SMT and encoding games
• Demos of Alive + use
• LLVM verification
• Alloy - requirements spec + model-finding + test gen
• To understand FOL
• To generate tests
• Hoare-logic
• Else I'll look bad if I let you interview and they find out
• Frama-C
• Get real !!

Syllabus (roughly)

​

• Weak memory models
• Floating-point verification
• Verification for ML
• ML to help verify
• Verify powered by RL
• Fuzzing
• PROJECTS
• and no more assignments
• Lectures + polls continue

Grades, Credits, discussions, cheating

​

• Cheating
• don't
• Discussions
• very freely
• Don't deprive your friend of the pleasure of solving
• Barring that, help
• But in small increments
• This gets my job done
• Do it on Piazza so that we are free and open
• And we can correct each other!
• Credits
• Always cite sources
• Grades (next slide)

Grades

​

• 50% for projects
• Group of 3 required minimum
• Upto 5
• Special cases allowed (ask and get permission)
• 30% for assignments
• Roughly once every week
• Different sizes
• Roughly 6
• 10% for quizzes
• Did you learn something over one week?
• What was it?
• 10% for polls
• Prime your mind BEFORE you come to the next class
• DUE BEFORE CLASS

Project suggestions + background survey

​

• See https://docs.google.com/document/d/1TJ_mndKG2gZqj6qmRHbGIDocl-qLGywX3nO7IoIUkgM/edit?usp=share_link

Resources

​

• Computer
• Your laptop or CADE
• Books
• I've kept enough online; more to come + papers then
• Office hours
• Me : 1245 to 145pm Tue and Thu
• T.M. Tanmay : ask him
• Class webpage
• Soon up as Google Site
• Slides linked to it
• Submissions
• Till project : Canvas
• Project : Git
• Piazza only way to communicate

spare

• C
• dd
• dd

​