Description
Motivation
Software systems are becoming an important part of the infrastructure
of our society. Correctness and reliability have become issues of outmost
importance. Testing and correction of software systems are irksome
processes which typically consume half of the resources for system
development. Thus, we need tools for
analyzing software systems with the purpose of checking that they
conform to their intended behavior, and for locating imperfections
(``bugs'') that will cause run-time errors, security vulnerabilities,
crashes, undelivered functionality, etc.
Topic
This course concentrates on techniques to verify and find bugs in
concurrent and parallel software systems. Problems that arise from the
parallel execution of several threads, processes, or components are
particularly hard to find a diagnose. In particular, the course teaches
model checking. Model checking techniques can automatically analyze
a pseudo-code description of a communication protocol, a concurrent algorithm,
etc. and find all potential errors. The course will also cover the basics of
structured testing for concurrent and parallel software.
Tool
The material will be practically demonstrated with the
tool SPIN. Spin supports a high level language to specify systems descriptions,
called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool checks the logical consistency of a specification. It reports on deadlocks, unspecified receptions, flags incompleteness, race conditions, and unwarranted assumptions about the relative speeds of processes.
Spin can also be used to illustrate techniques in structured software testing.
This year
we will direct particular attention to the analysis of concurrent multi-threaded algorithms. Such algorithms
are used to make programs more performant on multiprocessor architectures. In e.g., the {\tt java.util.concurrent}
package they are used to provide abstractions of common data structures (queues, sets, ...) which can be
accessed concurrently by several threads.