In this paper, we introduce Manim-DFA, an extension of the Manim library for generating video visualisations to teach data flow analysis and abstract interpretation. Despite the importance of data flow analysis in sta...
详细信息
data flow analysis is a technique essential to the compile-time optimization of computer programs, wherein facts relevant to program optimizations are discovered by the global propagation of facts obvious locally. Thi...
详细信息
data flow analysis is a technique essential to the compile-time optimization of computer programs, wherein facts relevant to program optimizations are discovered by the global propagation of facts obvious locally. This paper extends several known techniques for data flow analysis of sequential programs to the static analysis of distributed communicating processes. In particular, we present iterative algorithms for detecting unreachable program statements, and for determining the values of program expressions. The latter information can be used to place bounds on the size of variables and messages. Our main innovation is theevent spanning graph, which serves as a heuristic for ordering the nodes through which dataflow information is propagated. We consider bothstatic communication, where all channel arguments are constants, and the more difficultdynamic communication, where channel arguments may be variables and channels may be passed as messages.
Just-in-Time (JIT) compilation is frequently employed in order to speed-up the execution of platfor-independent and dynamically extensible mobile code applications. Since the time required for dynamic compilation dire...
详细信息
Just-in-Time (JIT) compilation is frequently employed in order to speed-up the execution of platfor-independent and dynamically extensible mobile code applications. Since the time required for dynamic compilation directly influences a program's execution time, JIT compilers usually utilize only simple and fast techniques for program analysis and optimization. To improve further the analysis and optimization process of such compilers program annotations can be used. However, mostly all current annotation approaches suffer from the fact that the verification of transmitted program information is time consuming and therefore will not be carried out on the consumer side of a mobile code system. In this paper, we present a verifiable annotation technique that is based on a well known iterative dataflow algorithm and which can be used for the transmission of all program information that can be derived through data flow analysis. Preliminary measurements of compilation and verification time indicate that the presented technique seems to be implementable and therefore could be used as an all-purpose transportation technique for safe program annotations.
In LOTOS, a system is specified as a behaviour expression describing the externally observable behaviour of the system in terms of possible sequences of interactions between the system and its environment. The desired...
详细信息
In LOTOS, a system is specified as a behaviour expression describing the externally observable behaviour of the system in terms of possible sequences of interactions between the system and its environment. The desired control flow and dataflow that must be established by a possible implementation of the system are specified in the behaviour expression as implicit enumerations of allowed sequences of interaction identifiers and relationships among interaction parameters, respectively. A model exposing the desired flow of data within the allowed control flow expressed in a system specification in LOTOS is presented. Based on the explicit information provided by the model, dataflow anomaly detection and dataflow oriented test selection are facilitated. A comprehensive example, i.e. an alternating bit protocol specification, is used to illustrate both these validation activities. An error in this specification is revealed by the analysis of a dataflow anomaly detected within the specification. A set of test paths is derived from the specification by the application of an existing dataflow oriented test selection criterion, called all-uses criterion.
Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain go...
详细信息
ISBN:
(数字)9783030720193
ISBN:
(纸本)9783030720193;9783030720186
Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Existing data flow analysis techniques do elide a subset of such infeasible paths, but have the restriction that they admit only finite abstract analysis domains. In this paper we propose a generalization of these approaches to admit infinite abstract analysis domains, as such domains are commonly used in practice to obtain high precision. We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to a baseline approach that does not elide any infeasible paths and to another baseline that elides infeasible paths but admits only finite abstract domains.
In this paper we describe an effective compile-time analysis for software prefetching in Java. Previous work in software data prefetching for pointer-based codes uses simple compiler algorithms and does not investigat...
详细信息
ISBN:
(纸本)0769513638
In this paper we describe an effective compile-time analysis for software prefetching in Java. Previous work in software data prefetching for pointer-based codes uses simple compiler algorithms and does not investigate prefetching for object-oriented language features that make compile-time analysis difficult. We develop a new dataflowanalysis to detect regular accesses to linked data structures in Java programs. We use intra and interprocedural analysis to identify profitable prefetching opportunities for greedy and jump-pointer prefetching, and we implement these techniques in a compiler for Java. Our results show that both prefetching techniques improve four of our ten programs. The largest performance improvement is 48% with jump-pointers, but consistent improvements are difficult to obtain.
data flow analysis as expressed by Monotone Frameworks is often associated with classical imperative programming languages and has played a crucial role in the efficient implementation of these languages. Robin Milner...
详细信息
ISBN:
(纸本)9783540713159
data flow analysis as expressed by Monotone Frameworks is often associated with classical imperative programming languages and has played a crucial role in the efficient implementation of these languages. Robin Milner's Calculus of Communicating Systems, CCS, is concerned with modelling concurrent systems and has mainly been analysed using types and control flow analyses. In the present paper we present an instance of a Monotone Framework together with a novel worklist algorithm for more precisely approximating the flow-sensitive control structure of even infinitary processes expressed in CCS.
The paper develops a framework that is based on the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are represented as models of...
详细信息
This paper introduces an approach to apply dataflow testing techniques to Abstract State Machines specifications. Since traditional dataflow coverage criteria are strictly based on the mapping between a program and ...
详细信息
ISBN:
(纸本)9783540876021
This paper introduces an approach to apply dataflow testing techniques to Abstract State Machines specifications. Since traditional dataflow coverage criteria are strictly based on the mapping between a program and its flow graph, they cannot be directly applied to AsMs. In this context we are interested hi tracing the flow of data, between states in ASM runs as opposed to between nodes in a program's flow graph. Therefore, we revise the classical concepts hi data How analysis and define them on two levels: the syntactic (title) level, and the computational (run) level. We also specify a family of ad hoc dataflow coverage criteria and introduce a model checking-based approach to generate automatically test cases satisfying a given set;of coverage criteria from ASM Models.
Executable modeling allows the models to be executed and treated as prototype to determine the behavior of a system. These models use precise action languages to specify the algorithms and computational details requir...
详细信息
ISBN:
(纸本)9783540690955
Executable modeling allows the models to be executed and treated as prototype to determine the behavior of a system. These models use precise action languages to specify the algorithms and computational details required for, execution. These action languages are developed on the basis of UML action semantics metamodel that provides the abstract syntax. The use of a concrete action language makes a traditional model work like an executable one. The actions specified by the action language might involve variables and their data values that are useful to be analyzed in terms of dataflow. In this paper, we provide data flow analysis (DFA) of the standard UML action semantics that can be used with executable models. The analysis provides a generic dataflow at the abstract syntax level and allows a mapping to any of the action languages providing the concrete syntax. Our approach does not focus on a particular action language;therefore it can easily be applied to any concrete syntax. We apply the proposed approach to a case study and identify the dataflow from executable UML state machine.
暂无评论