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 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.

翻译：最坏情况输入生成旨在自动生成能够展现程序最坏性能的输入。它具有多种应用，例如可用于检测拒绝服务攻击的潜在漏洞。然而，为并发程序生成最坏情况输入并非易事，特别是对于像内存这类资源，其峰值开销取决于进程的调度方式。本文提出了首个针对非单调资源度量（如内存）下并发程序的可靠最坏情况输入生成算法。其核心思想在于利用资源注释会话类型与符号执行。会话类型描述了进程演算中通道上的通信协议。通过配备资源注释，资源注释会话类型不仅能编码成本界限，还能指示进程间可重用和可转移的资源数量。这一信息对于在符号执行过程中识别最坏情况执行路径至关重要。该算法是可靠的：若其返回任何输入，则该输入保证为有效的最坏情况输入。该算法也具有相对完备性：只要资源注释会话类型具有足够的表达能力，且用于SMT求解的背景理论是可判定的，则保证能返回一个最坏情况输入。一个关于Web服务器内存使用的简单案例研究展示了该最坏情况输入生成算法的实用性。