Showing 1–2 of 2 results for author: Milanova, A

FlowCFL: A Framework for Type-based Reachability Analysis in the Presence of Mutable Data

Authors: Ana Milanova

Abstract: Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a framework for type-based reachability analysis in the presence of mutable data. Interestingly, the underlying semantics of FlowCFL is CFL-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability an… ▽ More Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a framework for type-based reachability analysis in the presence of mutable data. Interestingly, the underlying semantics of FlowCFL is CFL-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability analysis. Second, we establish correctness of CFL-reachability over graphs with inverse edges (inverse edges are necessary for the handling of mutable heap data). Our approach combines CFL-reachability with reference immutability to avoid the addition of certain infeasible inverse edges and we demonstrate empirically that avoiding those edges results in precision improvement. Our formal account of correctness extends to this case as well. Third, we present a type-based reachability analysis and establish equivalence between a certain CFL-reachability analysis and the type-based analysis, thus proving correctness of the type-based analysis. △ Less

Submitted 13 May, 2020; originally announced May 2020.

Formalizing Event-Driven Behavior of Serverless Applications

Authors: Matthew Obetz, Stacy Patterson, Ana Milanova

Abstract: We present new operational semantics for serverless computing that model the event-driven relationships between serverless functions, as well as their interaction with platforms services such as databases and object stores. These semantics precisely encapsulate how control transfers between functions, both directly and through reads and writes to platform services. We use these semantics to define… ▽ More We present new operational semantics for serverless computing that model the event-driven relationships between serverless functions, as well as their interaction with platforms services such as databases and object stores. These semantics precisely encapsulate how control transfers between functions, both directly and through reads and writes to platform services. We use these semantics to define the notion of the service call graph for serverless applications that captures program flows through functions and services. Finally, we construct service call graphs for twelve serverless JavaScript applications, using a prototype of our call graph construction algorithm, and we evaluate their accuracy. △ Less

Submitted 7 December, 2019; originally announced December 2019.