Abstract allocation as a unified approach to polyvariance in control-flow analyses

2018 ◽  
Vol 28 ◽  
Author(s):  
THOMAS GILRAY ◽  
MICHAEL D. ADAMS ◽  
MATTHEW MIGHT
Keyword(s):  
Design Space ◽  
Flow Analysis ◽  
Operational Semantics ◽  
Control Flow ◽  
Unified Approach ◽  
Abstract Machine ◽  
Abstract Machines ◽  
History Of ◽  
Concrete Operational ◽  
And Control

AbstractIn higher order settings, control-flow analysis aims to model the propagation of both data and control by finitely approximating program behaviors across all possible executions. The polyvariance of an analysis describes the number of distinct abstract representations, or variants, for each syntactic entity (e.g., functions, variables, or intermediate expressions). Monovariance, one of the most basic forms of polyvariance, maintains only a single abstract representation for each variable or expression. Other polyvariant strategies allow a greater number of distinct abstractions and increase analysis complexity with the aim of increasing analysis precision. For example, k-call sensitivity distinguishes flows by the most recent k call sites, k-object sensitivity by a history of allocation points, and argument sensitivity by a tuple of dynamic argument types. From this perspective, even a concrete operational semantics may be thought of as an unboundedly polyvariant analysis. In this paper, we develop a unified methodology that fully captures this design space. It is easily tunable and guarantees soundness regardless of how tuned. We accomplish this by extending the method of abstracting abstract machines, a systematic approach to abstract interpretation of operational abstract-machine semantics. Our approach permits arbitrary instrumentation of the underlying analysis and arbitrary tuning of an abstract-allocation function. We show that the design space of abstract allocators both unifies and generalizes existing notions of polyvariance. Simple changes to the behavior of this function recapitulate classic styles of analysis and yield novel combinations and variants.

scholarly journals The Perspective on Data and Control Flow Analysis in Topological Functioning Models by Petri Nets

2014 ◽  
Vol 16 (1) ◽  
pp. 77-84
Author(s):  
Erika Asnina ◽  
Begoña Cristina Pelayo García-Bustelo
Keyword(s):  
Petri Nets ◽  
Software Design ◽  
Algebraic Topology ◽  
Research Result ◽  
Flow Analysis ◽  
Control Flow ◽  
Colored Petri Nets ◽  
Data Flows ◽  
Definition Of ◽  
And Control

Abstract The perspective on integration of two mathematical formalisms, i.e., Colored Petri Nets (CPNs) and Topological Functioning Model (TFM), is discussed in the paper. The roots of CPNs are in modeling system functionality. The TFM joins principles of system theory and algebraic topology, and formally bridges the solution domain with the problem domain. It is a base for further automated construction of software design models. The paper discusses a perspective on check of control and data flows in the TFM by CPNs formalism. The research result is definition of mappings from TFMs to CPNs.

scholarly journals Flow Analysis of Lambda Expressions

1981 ◽  
Vol 10 (128) ◽  
Author(s):  
Neil D. Jones
Keyword(s):  
Programming Languages ◽  
Flow Analysis ◽  
Lambda Calculus ◽  
Control Flow ◽  
Point Of View ◽  
Approximate Description ◽  
Interprocedural Analysis ◽  
And Control ◽  
Lambda Expression ◽  
Parameter Transmission

<p>We describe a method to analyze the data and control flow during mechanical evaluation of lambda expressions. The method produces a finite approximate description of the set of all states entered by a call-by-value lambda-calculus interpreter; a similar approach can easily be seen to work for call-by-name. A proof is given that the approximation is ''safe'' i.e. that it includes descriptions of every intermediate lambda-expression which occurs in the evaluation.</p><p>From a programming languages point of view the method extends previously developed interprocedural analysis methods to include both local and global variables, call-by-name or call-by-value parameter transmission and the use of procedures both as arguments to other procedures and as the results returned by them.</p>

scholarly journals Inter-Deriving Semantic Artifacts for Object-Oriented Programming

2008 ◽  
Vol 15 (5) ◽  
Author(s):  
Olivier Danvy ◽  
Jacob Johannsen
Keyword(s):  
Operational Semantics ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Small Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Explicit Substitutions

We present a new abstract machine for Abadi and Cardelli's untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli's reduction semantics and natural semantics relative to each other. <br /> <br />To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli's untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.

scholarly journals Run-time Complexity Bounds Using Squeezers

2021 ◽  
pp. 320-347
Author(s):  
Oren Ish-Shalom ◽  
Shachar Itzhaky ◽  
Noam Rinetzky ◽  
Sharon Shoham
Keyword(s):  
Time Complexity ◽  
Fundamental Problem ◽  
Flow Analysis ◽  
Control Flow ◽  
Ranking Functions ◽  
Local Conditions ◽  
Data Dependencies ◽  
Complexity Bounds ◽  
Common Notion ◽  
And Control

AbstractDetermining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource complexity of programs that use integer values and linear arithmetic. Unfortunately, they fall short when execution traces become more involved, esp. when data dependencies may affect the termination conditions of loops. In such cases, state-of-the-art analyzers have shown to produce loose bounds, or even no bound at all.We propose a novel technique that generalizes the common notion of recurrence relations based on ranking functions. Existing methods usually unfold one loop iteration, and examine the resulting relations between variables. These relations assist in establishing a recurrence that bounds the number of loop iterations. We propose a different approach, where we derive recurrences by comparing whole traces with whole traces of a lower rank, avoiding the need to analyze the complexity of intermediate states. We offer a set of global properties, defined with respect to whole traces, that facilitate such a comparison, and show that these properties can be checked efficiently using a handful of local conditions. To this end, we adapt state squeezers, an induction mechanism previously used for verifying safety properties. We demonstrate that this technique encompasses the reasoning power of bounded unfolding, and more. We present some seemingly innocuous, yet intricate, examples where previous tools based on cost relations and control flow analysis fail to solve, and that our squeezer-powered approach succeeds.

Sign in / Sign up

Export Citation Format

Share Document