Abstract : This paper proposes a technique for estimating the computational time of programs in an actor model, which is intended to serve as a compiler target of a wide variety of actor-based programming languages. We define a compositional translation function returning cost equations, which are fed to an automatic off-the-shelf solver for obtaining the time bounds. Our approach is based on a new notion of synchronization sets, which captures possible difficult synchronization patterns between actors and helps make the analysis efficient and precise. The approach is proven to correctly over-approximate the worst computational time of an actor model of concurrent programs. Our technique is complemented by a prototype analyzer that returns upper bound of costs for the actor model.
https://hal.inria.fr/hal-02392909 Contributor : Laneve CosimoConnect in order to contact the contributor Submitted on : Wednesday, December 4, 2019 - 10:52:27 AM Last modification on : Wednesday, February 2, 2022 - 3:56:17 PM Long-term archiving on: : Thursday, March 5, 2020 - 5:17:31 PM
Cosimo Laneve, Michael Lienhardt, Ka Pun, Guillermo Román-Díez. Time analysis of actor programs. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2019, 105, pp.1 - 27. ⟨10.1016/j.jlamp.2019.02.007⟩. ⟨hal-02392909⟩