The aim of this paper is to present a new paradigm for reactive and real-time distributed programming: weak synchronism. We define a small language for communicating reactive automata, and characterize it by an operat...
详细信息
ISBN:
(纸本)0444817913
The aim of this paper is to present a new paradigm for reactive and real-time distributed programming: weak synchronism. We define a small language for communicating reactive automata, and characterize it by an operational semantics. We show that weak synchronism provides a deterministic semantics of concurrency and allows physical distributed implementations. This weak synchronous paradigm can then be extended to real-time programming, by defining a more general paradigm, a strong-weak synchronous coupling.
In 1974, Gilles Khan defined a seminal semantic model for asynchronous dataflow programming that would then be called as the eponymous Kahn process networks (KPN) and instantiated in as many models of the so-called DP...
详细信息
In 1974, Gilles Khan defined a seminal semantic model for asynchronous dataflow programming that would then be called as the eponymous Kahn process networks (KPN) and instantiated in as many models of the so-called DPN hierarchy as domain-specific fields of information processing from digital signal processing to hybrid cyber-physical systems. Among these, synchronous programming models have had an important impact in the specific domain of embedded software design. In this paper, we consider an instance of what seems to be one of the many synchronous models of computation: polychrony, initiated by the dataflow language Signal and its multi-clock (i.e. polychronous) model of computation and, later on, CCSL (clock constraints specification language). We provide an in-depth study of its semantic relationship with respect to the original definition of KPNs and hint toward the idea of polychrony as a methodology to locally synchronize (abstractions of) globally asynchronous processes. In particular, we formally define the property, referred to as "polyendochrony", that allows one to consider a given desynchronized network of synchronous Signal processes (a GALS architecture) as the implementation of a corresponding KPN model (an asynchronous network of Khandeterministic functions). For this class of networks, we formalize the Signal program analysis and transformations that define synchronous clusters of Signal processes of guaranteed deterministic behavior in an asynchronous network, that is, without synchronizing communications in the entire network. This definition yields a new strategy of multithreaded code generation that is available in the open-source Polychrony toolset of the Signal language and blurs the limits between the asynchronous and polychronous models of computation.
Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite se...
详细信息
Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first "state-free" model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.
We give a completion theorem for ordered magmas (i.e. ordered algebras with monotone operations) in a general form. Particular instances of this theorem are already known, and new results follow. The semantics of prog...
详细信息
We give a completion theorem for ordered magmas (i.e. ordered algebras with monotone operations) in a general form. Particular instances of this theorem are already known, and new results follow. The semantics of programming languages is the motivation of such investigations.
The programming logic PL/CV3 is based on the notion of a mathematical type. The core of the type theory, from which the full theory for program verification and specification can be derived, is presented. Whereas the ...
详细信息
Describes the use of grammar attributes for computer programminglanguages and compiler. Evaluation on the semantic attributes of programming; Relative efficiency of grammar attributes; Interrelation between syntactic...
详细信息
Describes the use of grammar attributes for computer programminglanguages and compiler. Evaluation on the semantic attributes of programming; Relative efficiency of grammar attributes; Interrelation between syntactic symbols and semantic functions.
作者：
WEGNER, ETECH UNIV BERLIN
INFORMATIK FORSCH GRP PROGRAM & COMPILEN 2ERNST REUTER PLATZ 8BERLIN 10WEST GERMANY
Describes a style of computer programming which combines the advantages of structured programming with nearly all the power of the jump. Gap between the adherents of structured programming and the devotees of the unre...
详细信息
Describes a style of computer programming which combines the advantages of structured programming with nearly all the power of the jump. Gap between the adherents of structured programming and the devotees of the unrestricted goto; Advantages of structured programming; Types of flowcharts used in decomposing an action; Limitations and drawbacks of the programming style.
It IS shown that two widely different notions of program equivalence coincide for the language of recurslve definitions with simplification rules The first is the now classical equivalence for fixed-point semantics. T...
详细信息
Following the fixpoint theory of Scott, the semantics of computer programs are defined in terms of the least fixpoints of recursive programs. This allows not only the justification of all existing verification techniq...
详细信息
Following the fixpoint theory of Scott, the semantics of computer programs are defined in terms of the least fixpoints of recursive programs. This allows not only the justification of all existing verification techniques, but also their extension to the handling, in a uniform manner of various properties of computer programs, including correctness, termination, and equivalence. [ABSTRACT FROM AUTHOR]
We consider three kinds of mathematical objects which can be designated as the “meaning” or “semantics” of programs: binary relations between initial and final states, binary relations on predicates (partial-corre...
详细信息
暂无评论