A denotational framework for comparing models of computation Daniele Gasperini Abstract Aim compare different model of computation and their certain essential features How use a denotational framework Main characteristics Denotational rather than operational Mathematical approach Main actors Processes Signals Events Tagged signal model SIGNALS 1 Event e tag value Set of values V Set of tags T Tags e TxV model time precedence relationships synchronization points Values represent operands and result of computation Signal s set of events subset of T x V SIGNALS 2 Characteristics notations Functional signals e1 t v1 s and e2 t v2 s then v1 v2 S the set of all signals SN collection tuple of N signals empty signal no events collection tuple of N empty signals S and SN bottom absence of value PROCESSES P process subset of SN for some N s behavior of a process s SN and s P P set of behaviors Composing processes Inputs and outputs Determinacy Composing processes 1 P set of behaviors s Composing P1 x P2 x Pn Given M processes in SN a process Q composed of these processes is given by Q Pi Pi P Where P is the collection of processes Pi S N 1 i M Composing processes 2 projections Let I i1 i m be an ordered set of indices in the range 1 i N and define the projection I s of s s1 s N SN onto Sm by I s s i1 s i m Process P set of behaviors s I P set s such that there exists s P where I s s Inputs and outputs Input to a process SN is an externally imposed constraint A S N such that A P is the total set of acceptable behaviors Set of all possible inputs is B S N I size m P O size n A process P is functional with respect to I O if for every s P and s P where I s I s it follows that O s O s There is a single valued mapping F Sm Sn such that for all s P o s F I s Determinacy A process is determinate if for any input A B it has exactly one behavior or exactly no behaviors Otherwise is nondeterminate functional functional functional preserve Depends on the tag system and the process Functional source processes with exacly one behavior functional preserve Tags systems The central role of a tag system is to establish ordering among events s1 s2 s3 specification i e time implementation s 1 s2 s3 Ordering relation among events properties Ordering of tags reflective Ordering of events transitive antisymmetric Timed models of computation The set of tags T is a totally ordered set Tag timestamp Flavors of timed models Metric time Continuous time Discrete event Discrete event simulators Synchronous and discrete time systems Sequential systems Metric time T totally ordered T Abelian group closed to addition zero for every t T there is another element t T such that t t 0 T has a metric Directly modeling physical systems Continuous time T totally ordered T is a continuum T s T for each signal s in any tuple s that satisfies the system Discrete event T totally ordered The set of tags must be a discrete subset of T The set of tags must be order isomorphic The timestamps that appear in any behavior can be enumerated in chronological order Many simulators most digital circuit simulators Discrete events simulators Same characteristics of discrete event Events explicitly include timestamp The simulator operates by keeping a list of events sorted by timestamp Delta time affects semantic and ensure strict causality Synchronous and discrete time systems Two events are synchronous if they have the same tag Two signals are synchronous if all events in one signal are synchronous with an event in the other signal and vice versa A process is synchronous if every signal in any behavior of the process is synchronous with every other signal in the behavior Sequential systems Single signal s The set of tags in the signal are totally ordered Untimed models of computation Tags are partially ordered Partial order is present in many models of computations because denotes Causality Synchronization Rendezvous of sequential processes Sequential processes reach a particular point at which they must verify that another process has reached a corresponding point before proceeding s1 T e1 T e2 T e3 s3 s2 Communicating sequential processes and the calculus of communicating systems Kahn process networks Processes communicate via channels which are one way unbounded FIFO queues with a single reader and a single writer FIFO T s is totally ordered for each signal s Imposes an ordering on the events Be s denote the sequence of values in s Two signals s and s sequence equivalent s s A process is sequence functional if given a set of equivalent tuples of input signals all possible outputs are sequence equivalent Sequence determinacy Dataflow Special case of Kahn process networks A dataflow process is a Kahn process that is also sequential Self loop signal is called firing signal s s P s e consumed by ei 1 e produced by ei ei e ei 1 ei e ei 1 Petri Nets Similar to dataflow Events within signals need not be ordered s1 s2 f s2 s1 such that f e e for all e s2 A firing an event in s2 has a corresponding token an event in s1 with a smaller tag Heterogeneous systems V divided into subsets carry the notion of data types T divided separately model parts of heterogeneous system continuous time discrete event and dataflow subsystems The Role of Tags in composition of processes Aim connect tagged signal model to well known results in semantics Two cases Discrete event systems Kahn process networks Discrete event systems Cantor metric Causality Synchronous events Distance of signals The n tuples of signals metric space Feedback loops Casual two possible outputs differ no earlier than the inputs that produced them Three form of causality If a process is functional and delta casual then the feedback loop has exactly one behavior Simulators VHDL Verilog Strictly casual two possible outputs differ later than the inputs that produced them or not at all Delta casual there is a delay of at least before any output of a process can be produced in reaction to an input event Monotonicity and continuity in Kahn process networks Causality a natural partial ordering for signals that contains a totally ordered set of events Prefix order s s s sequence of values in the signal s A process P is monotonic if it is a sequence functional Monotonicity Continuity with function F and F F s s A process P is continuous if it is a sequence functional with Determinacy Constructive procedure form function F of S m S n and for every chain W S feedback finding unique behavior F W
View Full Document
Unlocking...