Most programs are naturally designed over a variable number of discrete resources, which can be either physical components like threads or logical entities like context switches. Such a resource is typically parametric, where the value of the parameter varies across different execution environments and is unknown at design time. We call such programs resource-parameterized. Although highly desirable, formally analyzing resource-parameterized programs for various error conditions is notoriously hard or even undecidable. Some existing research imposes bounds on certain resources, such as the number of available execution threads or thread contexts, to tackle the intractability or sidestep the undecidability of the analysis. This leads to a series of incomplete techniques that are believed to catch “most bugs” in practice. The question whether these techniques can also prove the absence of bugs, however, has remained open in many cases.
We address this question by introducing a broad verification methodology, the paradigm of observation sequences, for resource-parameterized programs. The verification is conducted by observing how changes to the resource parameter affect the behavior of the considered program. Applied to the undecidable problem of context-parameterized analysis for procedural concurrent programs, the paradigm results in partial verification techniques: they may not terminate, but are able to both refute and prove safety for concurrent recursive threads. Experiments have shown the effectiveness of our techniques. The paradigm of observation sequences is designed with generality in mind. In this proposal, we plan to explore two more instances: one is the queue-parameterized analysis for message-passing programs which communicate via queued messages; the other is access-parameterized analysis for shared-memory multithreaded programs. Both generalizations are supported by tool development and empirical evaluation.