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服务器内存使用的简单案例研究验证了该最坏情况输入生成算法的实用性。