Mailbox Abstractions for Static Analysis of Actor Programs. Stiévenart, Q., Nicolay, J., De Meuter, W., & De Roover, C. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, volume 74, pages 25:1–25:30, Germany, 6, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi abstract bibtex Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.
@inproceedings{6f150759f01d485d91a9e97d6857ef7d,
title = "Mailbox Abstractions for Static Analysis of Actor Programs",
abstract = "Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.",
keywords = "Abstract interpretation, Abstraction, Actors, Mailbox, Static analysis",
author = "Quentin Sti{\'e}venart and Jens Nicolay and {De Meuter}, Wolfgang and {De Roover}, Coen",
year = "2017",
month = "6",
day = "1",
doi = "10.4230/LIPIcs.ECOOP.2017.25",
language = "English",
volume = "74",
pages = "25:1--25:30",
editor = "Peter M{\"u}ller",
booktitle = "31st European Conference on Object-Oriented Programming, ECOOP 2017",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
address = "Germany",
}
Downloads: 0
{"_id":"AnvDRs7gJtT8fDuZ2","bibbaseid":"stivenart-nicolay-demeuter-deroover-mailboxabstractionsforstaticanalysisofactorprograms-2017","author_short":["Stiévenart, Q.","Nicolay, J.","De Meuter, W.","De Roover, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Mailbox Abstractions for Static Analysis of Actor Programs","abstract":"Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.","keywords":"Abstract interpretation, Abstraction, Actors, Mailbox, Static analysis","author":[{"firstnames":["Quentin"],"propositions":[],"lastnames":["Stiévenart"],"suffixes":[]},{"firstnames":["Jens"],"propositions":[],"lastnames":["Nicolay"],"suffixes":[]},{"propositions":[],"lastnames":["De Meuter"],"firstnames":["Wolfgang"],"suffixes":[]},{"propositions":[],"lastnames":["De Roover"],"firstnames":["Coen"],"suffixes":[]}],"year":"2017","month":"6","day":"1","doi":"10.4230/LIPIcs.ECOOP.2017.25","language":"English","volume":"74","pages":"25:1–25:30","editor":[{"firstnames":["Peter"],"propositions":[],"lastnames":["Müller"],"suffixes":[]}],"booktitle":"31st European Conference on Object-Oriented Programming, ECOOP 2017","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","address":"Germany","bibtex":"@inproceedings{6f150759f01d485d91a9e97d6857ef7d,\n title = \"Mailbox Abstractions for Static Analysis of Actor Programs\",\n abstract = \"Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.\",\n keywords = \"Abstract interpretation, Abstraction, Actors, Mailbox, Static analysis\",\n author = \"Quentin Sti{\\'e}venart and Jens Nicolay and {De Meuter}, Wolfgang and {De Roover}, Coen\",\n year = \"2017\",\n month = \"6\",\n day = \"1\",\n doi = \"10.4230/LIPIcs.ECOOP.2017.25\",\n language = \"English\",\n volume = \"74\",\n pages = \"25:1--25:30\",\n editor = \"Peter M{\\\"u}ller\",\n booktitle = \"31st European Conference on Object-Oriented Programming, ECOOP 2017\",\n publisher = \"Schloss Dagstuhl - Leibniz-Zentrum f{\\\"u}r Informatik\",\n address = \"Germany\",\n}","author_short":["Stiévenart, Q.","Nicolay, J.","De Meuter, W.","De Roover, C."],"editor_short":["Müller, P."],"key":"6f150759f01d485d91a9e97d6857ef7d","id":"6f150759f01d485d91a9e97d6857ef7d","bibbaseid":"stivenart-nicolay-demeuter-deroover-mailboxabstractionsforstaticanalysisofactorprograms-2017","role":"author","urls":{},"keyword":["Abstract interpretation","Abstraction","Actors","Mailbox","Static analysis"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://soft.vub.ac.be/~cderoove/works.bib","dataSources":["abyQtmN3vDJoFXPPD"],"keywords":["abstract interpretation","abstraction","actors","mailbox","static analysis"],"search_terms":["mailbox","abstractions","static","analysis","actor","programs","stiévenart","nicolay","de meuter","de roover"],"title":"Mailbox Abstractions for Static Analysis of Actor Programs","year":2017}