Python is a popular programming language whose performance is known to be uncompetitive in comparison to static languages such as C. Although significant efforts have already accelerated implementations of the languag...
详细信息
ISBN:
(纸本)9798400703966
Python is a popular programming language whose performance is known to be uncompetitive in comparison to static languages such as C. Although significant efforts have already accelerated implementations of the language, more efficient ones are still required. The development of such optimized implementations is nevertheless hampered by its complex semantics and the lack of an official formal semantics. We address this issue by presenting an approach to define an executable semantics targeting the development of optimizing compilers. This executable semantics is written in a format that highlights type checks, primitive values boxing and unboxing, and function calls, which are all known sources of overhead. We also present semPy, a partial evaluator of our executable semantics that can be used to remove redundant operations when evaluating arithmetic operators. Finally, we present Zipi, a Python optimizing compiler prototype developed with the aid of semPy. On some tasks, Zipi displays performance competitive with that of state-of-the-art Python implementations.
D-Clean primitives are first class citizens which allows the coordination of a dynamical work distributions over a cluster. The computations are distributed automatically over the Grid by the middleware system. The pr...
详细信息
D-Clean primitives are first class citizens which allows the coordination of a dynamical work distributions over a cluster. The computations are distributed automatically over the Grid by the middleware system. The programmer controls the computation nodes in the generated boxes and the communication on the generated channels. In order to obtain highly abstract description about how the coordination primitives work, a generic model of the executable semantics is needed. This paper provides a more general version of the simulation of the real parallel computation in the D-Clean extension of the Clean language. First, the executable semantics definition for each D-Clean primitive is given in an abstract way. Second, we describe a graphical system that generates the computation scheme visualizing the maximum amount of parallelism. Finally, we state properties of the executable description of the distributed system designed for D-Clean and D-Box.
The Orc calculus is a simple, yet powerful theory of concurrent computations with great versatility and practical applicability to a very wide range of applications, as it has been amply demonstrated by the Orc langua...
详细信息
The Orc calculus is a simple, yet powerful theory of concurrent computations with great versatility and practical applicability to a very wide range of applications, as it has been amply demonstrated by the Orc language, which extends the Orc calculus with powerful programming constructs that can be desugared into the underlying formal calculus. This means that for: (i) theoretical, (ii) program verification, and (iii) language implementation reasons, the formal semantics of Orc is of great importance. Furthermore, having a semantics of Orc that is executable is essential to provide: (i) a formally-defined interpreter against which language implementations can be validated, and (ii) a (semi-)automatic way of generating a wide range of semantics-based program verification tools, including model checkers and theorem provers. This work proposes a formal executable semantics for Orc in rewriting logic, to support formal verification of Orc programs and to make possible semantics-based correct-by-construction Orc implementations. While being a very simple calculus, Orc has a quite subtle semantics, so that fully capturing all its semantic aspects is highly nontrivial. The two main sources of subtlety are: (i) its real-time semantics, and (ii) the priority of internal computations within an Orc expression over external computations that process responses from external sites. In this paper, we show a simple and elegant way of handling these two sources of subtlety in rewriting logic using an order-sorted type system supporting subtypes and subtype polymorphism, and "tick" rewrite rules for capturing time. Moreover, our rewriting semantics incorporates useful semantic equivalences between Orc programs as equations and equational attributes, making the semantics both more abstract and more efficient. The semantics of Orc is given in two different styles: (i) an SOS style, which is directly based on the original SOS of Orc, whose correctness follows immediately by constructio
We present a semantics of a significant fragment of the C programming language as described by the C11 standard. It consists of a small step semantics of a core language, which uses a structured memory model to captur...
详细信息
ISBN:
(纸本)9781450332965
We present a semantics of a significant fragment of the C programming language as described by the C11 standard. It consists of a small step semantics of a core language, which uses a structured memory model to capture subtleties of C11, such as strict-aliasing restrictions related to unions, that have not yet been addressed by others. The semantics of actual C programs is defined by translation into this core language. We have an explicit type system for the core language, and prove type preservation and progress, as well as type correctness of the translation. Due to unspecified order of evaluation, our operational semantics is non-deterministic. To explore all defined and undefined behaviors, we present an executable semantics that computes a stream of finite sets of reachable states. It is proved sound and complete with respect to the operational semantics. Both the translation into the core language and the executable semantics are defined as Coq programs. Extraction to OCaml is used to obtain a C interpreter to run and test the semantics on actual C programs. All proofs are fully formalized in Coq.
暂无评论