Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics

TL;DR

This work addresses generating inputs that trigger the worst-case memory usage in concurrent programs, a problem complicated by non-monotone resource metrics and scheduling. It introduces resource-annotated session types and session skeletons to guide symbolic execution, enabling sound evaluation of high-water-mark costs and transfer of potential across processes. The authors prove soundness and relative completeness of the approach and validate it with a web server case study, showing how independent versus scheduled sessions impact memory peaks. The framework enables detecting memory-related vulnerabilities to DoS-like scenarios in concurrent systems and provides a foundation for future enhancements in handling interdependence between input/output across channels.

Abstract

Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vulnerabilities to denial-of-service (DoS) attacks. However, it is non-trivial to generate worst-case inputs for concurrent programs, particularly for resources like memory where the peak cost depends on how processes are scheduled. This article presents the first sound worst-case input generation algorithm for concurrent programs under non-monotone resource metrics like memory. The key insight is to leverage resource-annotated session types and symbolic execution. Session types describe communication protocols on channels in process calculi. Equipped with resource annotations, resource-annotated session types not only encode cost bounds but also indicate how many resources can be reused and transferred between processes. This information is critical for identifying a worst-case execution path during symbolic execution. The algorithm is sound: if it returns any input, it is guaranteed to be a valid worst-case input. The algorithm is also relatively complete: as long as resource-annotated session types are sufficiently expressive and the background theory for SMT solving is decidable, a worst-case input is guaranteed to be returned. A simple case study of a web server's memory usage demonstrates the utility of the worst-case input generation algorithm.

Figures (17)

• Figure 1: (a) Process $P$ uses channel $c_1$ as a client and provides channel $c_2$. A dot on a channel denotes the channel's provider. (b) General SILL program consisting of multiple concurrent processes An internal channel connects two processes; an external channel connects a process with the external world.
• Figure 2: (a) Tight cost bound when all potential is supplied at once. The red dashed arrow indicates the potential supplied by the external world. (b) Tight cost bound when potential is supplied gradually. (c) Loose cost bound. Potential zero is never reached after the last injection of potential. So we can lower the cost bound (i.e., shorten the second and third red dashed arrows) without plunging into negative potential.
• Figure 3: (a) Concurrent processes $P_1$ and $P_2$. Time passes by in the direction of arrows. (b) Results of global tracking and local tracking.
• Figure 4: (a) The potential helps us derive the correct high-water mark. A rectangle next to an arrow represents the potential during the arrow's time period. The number inside a rectangle and its length indicate the amount of potential. If no rectangle exists, it indicates zero potential. (b) Same diagram as (a), but the potential is colored red and blue.
• Figure 5: (a) Red potential in the process $P_2$ is not entirely consumed. Red hatched rectangles and blue blank rectangles represent red and blue potential, respectively. (b) Blue potential is generated in the process $P_1$ before red potential is consumed in the process $P_2$. But some blue potential is left unconsumed in the process $P_1$.

Theorems & Definitions (24)

• Theorem 3.1: Soundness of resource-aware SILL Das2018Das2019
• Definition 5.1: Happened-before relation Lamport1978
• Definition 5.2: Synchronization of two processes
• Theorem 5.3: Checking tightness of cost bounds
• Definition 5.4: Cost bounds of skeletons
• Definition 5.5: Cost bounds of configurations
• Definition 5.6: Similarity between predicates
• Proposition 5.7: Simulation for soundness
• Theorem 5.8: Soundness of worst-case input generation
• proof