1. optimization
2. correctness

Some optimization examples:

• common subexpression elimination using available expression analysis
  • avoid recomputing (automatically or manually generated) identical expressions
• constant propagation
  • use constants instead of variables if variable value is known
• copy propagation
  • use another variable with the same name
• dead code elimination
  • remove unnecessary code
• automatically generate code for parallel machines

Consider code:

  c = a.next;

  x = complexComputationF(a.f,b.g);
  y = complexComputationG(c.f,d.g);
  z = x + y;
  c.f = e;
  u = complexComputationF(a.f,b.g);

Questions:

• can we compute complexComputationF and complexComputationG in parallel?
• does u compute same results as x ?
• what areas of memory do functions
  • read
  • write
• can a and c both refer to the same object?
  • alias analysis

References:

• Advanced Compiler Design and Implementation, By Steven S. Muchnick
• Tiger book, Chapter 17
• Publications on Jikes Java System
• Compilers: Principles, Techniques, and Tools (2nd Edition) by Alfred V. Aho, Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman
• Automatic parallelization of divide and conquer algorithms by Radu Rugina and Martin Rinard

Perform various partial correctness checks:

• initialization analysis
• protocol usage analysis
• array bounds checks
• absence of memory errors

Slides Illustrating Past Disasters

Software is used safety-critical systems (airplanes, cars, submarines). The consequences of errors are more severe than on desktops, so correctness standards must be higher. At the same time, complexity of systems bugs are more and more likely. In absence of automated tool support, disasters will happen. Here are examples of disasters:

• Between June 1985 and January 1987, six known accidents involved massive overdoses by the Therac-25 -- with resultant deaths and serious injuries, see also recent NYT article
• A kidney transplant patient was forced to have the new organ removed when it was discovered that the patient's blood type had been incorrectly recorded on a computer database
• US: The Fatal Flaws in the Patriot Missile System by Jeffrey St. Clair, Counterpunch April 17th, 2003. On March 24, a Patriot missile battery near the Kuwait border locked onto a British Royal Air Force Tornado G-4 jet that was returning from a raid on Basra. Four Patriot missiles were fired and one hit the jet, destroying the plane and killing two British pilots. Two days later, the radar for another Patriot missile battery locked on to a US F-16. The pilot of fighter jet located the radar dish and destroyed it. Then on April 2 an U.S. Navy F/A-18 Hornet was shot down by another Patriot missile, killing the pilot. “They're looking into a software problem,” said Navy Lt. Commander Charles Owens.
• Software Bug Causes Train Wreck

Large commercial losses:

• Pentium bugs encouraged hardware industry to embrace verification
• Northeast blackout in USA, April 2003
• Millions of bank accounts were impacted by errors due to installation of inadequately tested software code in the transaction processing system of a major North American bank, according to mid-2004 news reports. Articles about the incident stated that it took two weeks to fix all the resulting errors, that additional problems resulted when the incident drew a large number of e-mail phishing attacks against the bank's customers, and that the total cost of the incident could exceed $100 million.

For many more examples, see

• Collection of Software Bugs by Prof. Thomas Huckle
• Lecture by Prof. Thomas Henzinger
• Illustrative Risks by Peter G. Neumann, some of which are explained in more detail in Forum On Risks To The Public In Computers And Related Systems
• Some Recent Software Failures Caused by Software Bugs
• A Collection of Well-Known Software Failures

“In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any run-time error in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).”

• http://www.astree.ens.fr/
• PLDI 2003 Paper on Astree
• How does the ASTREE analyzer deal with digital filters? a talk video

• Static Driver Verifier, which grew out of the SLAM Project and is related the BLAST Project

• Modular checking for buffer overflows in the large Brian Hackett, Manuvir Das, Daniel Wang, Zhe Yang

• 7 April 2005. AbsInt contributes to guaranteeing the safety of the A380, the world's largest passenger aircraft. The Analyzer is able to verify the proper response time of the control software of all components by computing the worst-case execution time (WCET) of all tasks in the flight control software. This analysis is performed on the ground as a critical part of the safety certification of the aircraft.

• Coverity Prevent SAN FRANCISCO - January 8, 2008 - Coverity®, Inc., the leader in improving software quality and security, today announced that as a result of its contract with US Department of Homeland Security (DHS), potential security and quality defects in 11 popular open source software projects were identified and fixed. The 11 projects are Amanda, NTP, OpenPAM, OpenVPN, Overdose, Perl, PHP, Postfix, Python, Samba, and TCL.
  • recently: bugs in Android kernel