Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
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...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2024-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | http://lmcs.episciences.org/12242/pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849344800712556544 |
|---|---|
| author | Long Pham Jan Hoffmann |
| author_facet | Long Pham Jan Hoffmann |
| author_sort | Long Pham |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-63cbbff2deff4a808c90043c3f5ffc46 |
| institution | Kabale University |
| issn | 1860-5974 |
| language | English |
| publishDate | 2024-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj-art-63cbbff2deff4a808c90043c3f5ffc462025-08-20T03:42:35ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742024-12-01Volume 20, Issue 410.46298/lmcs-20(4:26)202412242Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource MetricsLong PhamJan HoffmannWorst-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.http://lmcs.episciences.org/12242/pdfcomputer science - programming languagescomputer science - distributed, parallel, and cluster computingcomputer science - logic in computer science |
| spellingShingle | Long Pham Jan Hoffmann Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics Logical Methods in Computer Science computer science - programming languages computer science - distributed, parallel, and cluster computing computer science - logic in computer science |
| title | Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics |
| title_full | Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics |
| title_fullStr | Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics |
| title_full_unstemmed | Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics |
| title_short | Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics |
| title_sort | worst case input generation for concurrent programs under non monotone resource metrics |
| topic | computer science - programming languages computer science - distributed, parallel, and cluster computing computer science - logic in computer science |
| url | http://lmcs.episciences.org/12242/pdf |
| work_keys_str_mv | AT longpham worstcaseinputgenerationforconcurrentprogramsundernonmonotoneresourcemetrics AT janhoffmann worstcaseinputgenerationforconcurrentprogramsundernonmonotoneresourcemetrics |