Actor languages model concurrency as processes that communicate through asynchronous message sends. Unfortunately, as the complexity of these systems increases, it becomes more difficult to compose and integrate their...
详细信息
Actor languages model concurrency as processes that communicate through asynchronous message sends. Unfortunately, as the complexity of these systems increases, it becomes more difficult to compose and integrate their components. This is because of assumptions made by components about their communication partners which may not be upheld when they remain implicit. In this paper, we bring design-by-contract programming to actor programs through a contract system that enables expressing constraints on receiver-related properties. Expressing properties about the expected receiver of a message, and about this receiver's communication behavior, requires two novel types of contracts. Through their recursive structure, these contracts can govern entire communication chains. We implement the contract system for an actor extension of Scheme, describe it formally, and show how to assign blame in case of a contract violation. Finally, we prove our contract system and its blame assignment correct by formulating and proving a blame correctness theorem.
Design-by-contract is a software engineering practice where programmers annotate program elements with contract specifications that make expectations towards the user and supplier of the program element explicit. This...
详细信息
ISBN:
(纸本)9798400706127
Design-by-contract is a software engineering practice where programmers annotate program elements with contract specifications that make expectations towards the user and supplier of the program element explicit. This practice has been applied in various contexts such as higher-order programminglanguages. However, support for contracts in distributed actor programs is limited. Unfortunately, contract specifications need to be checked while executing the program which introduces a substantial overhead. To counter this, soft verification techniques have been proposed to verify (parts of) contract specifications, but have only been applied in the context of sequential programs. The goal of our research is therefore twofold: designing contract languages for distributed actor programs and developing techniques for their soft verification. In this context, we present a work plan and method, and show our preliminary results.
The relation between a structure and the function it runs is of interest in many fields, including computer science, biology (organ vs. function) and psychology (body vs. mind). Our paper addresses this question with ...
详细信息
The relation between a structure and the function it runs is of interest in many fields, including computer science, biology (organ vs. function) and psychology (body vs. mind). Our paper addresses this question with reference to computer science recent hardware and software advances, particularly in areas as Robotics, Self-Adaptive Systems, IoT, CPS, AI-Hardware, etc. At the modelling, conceptual level our main contribution is the introduction of the concept of "virtual organism" (VO), to populate the intermediary level between reconfigurable hardware agents and intelligent, adaptive software agents. A virtual organism has a structure, resembling the hardware capabilities, and it runs low-level functions, implementing the software requirements. The model is compositional in space (allowing the virtual organisms to aggregate into larger organisms) and in time (allowing the virtual organisms to get composed functionalities). The virtual organisms studied here are in 2D (two dimensions) and their structures are described by 2D patterns (adding time, we get a 3D model). By reconfiguration an organism may change its structure to another structure in the same 2D pattern. We illustrate the VO concept with a few increasingly more complex VO's dealing with flow management or a publisher-subscriber mechanism for handling services. We implemented a simulator for a VO, collecting flow over a tree-structure (TC-VO), and the quantitative results show reconfigurable structures are better suited than fixed structures in dynamically changing environments. Finally, we briefly show how Agapia - a structured parallel, interactive programming language where dataflow and control flow structures can be freely mixed - may be used for getting quick implementations for VO's simulation.
Apache Spark is a Big Data framework for working on large distributed datasets. Although widely used in the industry, it remains rather limited in the academic community or often restricted to software engineers. The ...
详细信息
Apache Spark is a Big Data framework for working on large distributed datasets. Although widely used in the industry, it remains rather limited in the academic community or often restricted to software engineers. The goal of this paper is to show with practical uses-cases that the technology is mature enough to be used without excessive programming skills by astronomers or cosmologists in order to perform standard analyses over large datasets, as those originating from future galaxy surveys. To demonstrate it, we start from a realistic simulation corresponding to 10 years of LSST data taking (6 billions of galaxies). Then, we design, optimize and benchmark a set of Spark python algorithms in order to perform standard operations as adding photometric redshift errors, measuring the selection function or computing power spectra over tomographic bins. Most of the commands execute on the full 110 GB dataset within tens of seconds and can therefore be performed interactively in order to design full-scale cosmological analyses. A jupyter notebook summarizing the analysis is available at https://***/astrolabsoftware/1807.03078. (C) 2019 Elsevier B.V. All rights reserved.
This paper describes the features of a scripting language proposed to support the practical implementation of agents and multi-agent systems using an agent-oriented programming approach. Agents are programmed in terms...
详细信息
ISBN:
(纸本)9781450360661
This paper describes the features of a scripting language proposed to support the practical implementation of agents and multi-agent systems using an agent-oriented programming approach. Agents are programmed in terms of procedures to be executed when interesting events occur, and the language provides specific constructs to describe managed events and related procedures. Among possible events, those related to communication are supported by specific constructs because of their relevance for the implementation of multi-agent systems. The proposed language is characterised by a strongly expressive syntax largely inspired by modern scripting languages to promote readability and to make agent programs similar to pseudocodes. Such a feature ensures that the programmer can use the language to describe the reactions of agents to events at a high level of abstraction, with all the advantages that it brings in terms of software quality.
We have developed a new programming language for implementing distributed algorithms encoded by means of local computations [17]. This language, called Lidia, is based on a two-level transition system model: the first...
详细信息
ISBN:
(纸本)0769521606
We have developed a new programming language for implementing distributed algorithms encoded by means of local computations [17]. This language, called Lidia, is based on a two-level transition system model: the first level is used to specify the behavior of each single component, whereas the second level captures their interactions. Transitions are basically expressed in a precondition-effect style. Lidia depends on a logic,L*(infinity) that is used to express the preconditions of each transition. The main topic of this paper is to present the L*(infinity) language and to bring out some of its basic properties. Moreover we will take advantage of these properties to define a class of distributed algorithms encoded by means of local computations, that can be implemented in our programming language. The completeness of Lidia, related to the use of users defined functions, will represent the main result of this paper.
Global predicates in distributed systems are predicates considering the state of more than one process. They are a useful concept for debugging parallel programs, e.g., for specifying assertions, breakpoints or termin...
详细信息
ISBN:
(纸本)0769521606
Global predicates in distributed systems are predicates considering the state of more than one process. They are a useful concept for debugging parallel programs, e.g., for specifying assertions, breakpoints or termination. In this paper we propose an algorithm for detecting the validity of local and global state predicates in distributed algorithms encoded by means of local computations. This algorithm is based on ideas introduced by Cooper and Marzullo and on the approach of Garg and Waldecker. It uses the Lamport's happened-before ordering relationship to construct a partial sorted sequence of all the events that have changed the local state of any process during a computation. While the sequence is traversed, all the global states through which the system has passed are computed and the validity of the given properties is checked. Under the same assumptions, our algorithm is significantly more efficient than the algorithms by Cooper and Marzullo and by Garg and Waldecker.
This paper presents a method for mechanically proving the soundness of a programming logic for a distributedprogramming language, in support of the development of verified program verification tools. We focus on: (1)...
详细信息
This paper presents a method for mechanically proving the soundness of a programming logic for a distributedprogramming language, in support of the development of verified program verification tools. We focus on: (1) how to formalize the operational semantics of a distributedprogramming language;(2) how to formalize the concept of program correctness for distributed programs;(3) how to mechanically prove the soundness of a programming logic with respect to the formal semantics of the language;(4) how to use the mechanized and sound logic to develop verification tools with soundness guaranteed;and (5) how to accomplish all above in the same formalism. Our programming logic permits the verification of single processes executing in isolation and, also, the verification of the composition of concurrently executing processes. Our method demonstrates that structuring the specification of operational semantics can ease the creation of a sound and mechanized programming logic for distributed programming languages. We believe that our method can be scaled up to larger distributed programming languages and their programming logics. The Cambridge HOL theorem proving system is used in our research. (C) 1999-Elsevier Science B.V. All rights reserved.
A programming language can provide much better support for interprocess communication than a library package can. Most message-passing languages limit this support to communication between the pieces of a single progr...
详细信息
A programming language can provide much better support for interprocess communication than a library package can. Most message-passing languages limit this support to communication between the pieces of a single program, but this need not be the case. Lynx facilitates convenient, typesafe message passing not only within applications, but also between applications and among distributed collections of servers. Specifically, it addresses issues of compiler statelessness, late binding, and protection that allow run-time interaction between processes that were developed independently and that do not trust each other. Implementation experience with Lynx has yielded important insights into the relationship between distributed operating systems and language run-time support packages and into the inherent costs of high-level message-passing semantics.
SR is a language for programmingdistributed systems ranging from operating systems to application programs. On the basis of our experience with the initial version, the language has evolved considerably. In this pape...
详细信息
SR is a language for programmingdistributed systems ranging from operating systems to application programs. On the basis of our experience with the initial version, the language has evolved considerably. In this paper we describe the current version of SR and give an overview of its implementation. The main language constructs are still resources and operations. Resources encapsulate processes and variables that they share; operations provide the primary mechanism for process interaction. One way in which SR has changed is that both resources and processes are now created dynamically. Another change is that inheritance is supported. A third change is that the mechanisms for operation invocation—call and send—and operation implementation—proc and in—have been extended and integrated. Consequently, all of local and remote procedure call, rendezvous, dynamic process creation, asynchronous message passing, multicast, and semaphores are supported. We have found this flexibility to be very useful for distributedprogramming. Moreover, by basing SR on a small number of well-integrated concepts, the language has proved easy to learn and use, and it has a reasonably efficient implementation.
暂无评论