forsyde-atom-0.2.2.1: Shallow-embedded DSL for modeling cyber-physical systems

Copyright(c) George Ungureanu 2015-2018
LicenseBSD-style (see the file LICENSE)
Maintainerugeorge@kth.se
Stabilityexperimental
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

ForSyDe.Atom

Description

The "spiritual parent" of this modeling framework dates as back as [Sander04] which presented ForSyDe, an EDSL for describing heterogeneous systems as networks of processes communicating through signals. In ForSyDe, processes alone capture the timing semantics of execution and synchronization according to a certain model of computation (MoC). The shallow implementation of ForSyDe, forsyde-shallow provides libraries of higher-order functions for instantiating processes called process constructors for several MoCs. The formal foundation upon which ForSyDe defines its semantics is the tagged signal model [Lee98], which is a denotational framework introduced by Lee and Sangiovanni-Vincentelli as a common meta model for describing properties of concurrent systems in terms of their behavior.

The forsyde-atom project started as a proof-of-concept for the atom-based approach to cyber-physical systems (CPS) introduced in [Ungureanu17]. This approach extends the ideas of the tagged signal model by systematically deconstructing processes to their basic semantics and recreating them using a minimal language of primitive building blocks called atoms. It also expands the scope of this model by exploiting more aspects of cyber-physical systems than just timing, but also adding primitives for parallelism, behavior extensions, etc, each in its own interacting environment called layer. You can read more about layers in the corresponding section further on.

The API documentation is structured as follows: this page provides an overview of the general notions and concepts, introducing the separate modules and the motivation behind them. Each major module corresponds to a separate layer described by a type class, and contains a number of sub-modules, mainly providing instances and helpers for their respective layer. The documentation for each module contains in-depth knowledge and examples. For more complex examples and tutorials follow the links in the project web page.

IMPORTANT!!! All multi-argument functions and utilities provided by the forsyde-atom API are named along the lines of functionMN where M represents the number of curried inputs (i.e. a1 -> a2 -> ... -> aM), while N represents the number of tupled outputs (i.e. (b1,b2,...,bN)). To avoid repetition we only provide documentation for functions with 2 inputs and 2 outputs (i.e. function22). In case the provided functions do not suffice, feel free to implement your own patterns following the examples in the source code.

Synopsis

The layered process model

The forsyde-atom project is led by three main policies:

  1. in order to cope with the complexity of cyber-physical systems (CPS) it tries to separate the concerns such as computation, timing, synchronization, parallelism, structure, behavior, etc.
  2. in order to have a small, ideally minimal grammar to reason about systems correctness, it aims to provide primitive (indivisible) operators called atoms as building blocks for independently developing complex aspects of a system's execution through means of composition or generalization.
  3. in order to express complex behaviors with a minimal grammar, it decouples structure (composition) from meaning (semantics), the only semantics carriers being atoms. Thus complex behaviors can be described in terms of patterns of atoms. Using ad-hoc polymorphism, atoms can be overloaded with different semantics triggered by the data type they input, whereas their composition is always the same.
atom
the elementary (primitive, indivisible) constructor which embeds a set of semantics relevant for their respective layer (e.g. timing, behavioural, structural, etc.)
atom patterns
meaningful compositions of atoms. They are provided as constructors which need to be properly instantiated in order to be used. We also use the term "pattern" to differentiate atom compositions as constructors from atoms as constructors.

The first policy, i.e. the separation of concerns led to the so-called layered process model which is reflected in the library by providing separate major modules associated with each layer. Layers as such are independent collections of entities for modeling different aspects of CPS. These aspects interact through means of higher-order functions, wrapping each other in as structured fashion in a way which can be visualized as below.

Layers are implemented as type classes which define:

  • atoms as function signatures belonging to the type class;
  • patterns which are compositions atoms, provided as (functional block) constructors, e.g. process constructors in the MoC layer;
  • data types for all the classes of behaviors concerning the aspect described by the layer in question. These types instantiate their respective type class and overload the atoms with semantics in accordance to the behavior described. For example, the MoC layer is currently instantiated by types describing the CT, DE, SY and SDF MoCs.

In order to model interleaving aspects of CPS, layers interact with each other through means of higher order functions. As such, each layer describes some atoms as higher-order functions which take entities belonging to another layer as arguments. Intrinsically, the data types belonging to a layer may be wrapping types of other layers, as depicted in the figure above. For a short comprehensive overview on layers, please refer to [Ungureanu17].

By convention, the first (innermost) layer is always the function layer which describes arbitrary functions on data and expresses the system's functional aspects. In the following paragraphs we will give an overview of the "outer" layers currently implemented in forsyde-atom, which in comparison, express the extra-functional aspects of a system (timing, behavior, synchronization, and so on).

The Extended Behavior (ExB) Layer

As seen in layered process model, the extended behavior layer expands the set of possible behaviors implied by a layer (typically the function layer), by defining a set of symbols with known semantics, and adding it to the pool of possible values or states.

While semantically the ExB layer extends the value pool in order to express special events (e.g. protocol, error messages or even the complete absence of events), it practically provides an independent environment to model events with a default/known response, independently of the data path. These responses are particularly captured by ExB atoms, thus enforcing the high-level separation of concerns between e.g. control and data paths.

This layer provides:

  • a set of extended behavior atoms defining the interfaces for the resolution and response functions, as part of the ExB type class (see below).
  • a library of function wrappers as specific atom patterns (check the ForSyDe.Atom.ExB module).
  • a set of data types defining classes of behaviors and instantiating the ExB type class (check the instances).

class Functor b => ExB b where Source #

Class which defines the atoms for the extended behavior layer.

As its name suggests, this layer is extending the behavior of the wrapped entity/function by expanding its domains set with symbols having clearly defined semantics (e.g. special events with known responses).

The types associated with this layer can simply be describes as:

where \(\alpha\) is a base type and \(b\) is the type extension, i.e. a set of symbols with clearly defined semantics.

Extended behavior atoms are functions of these types, defined as interfaces in the ExB type class.

Minimal complete definition

extend, (/.\), (/*\), (/&\), (/!\)

Methods

extend :: a -> b a Source #

Extends a value (from a layer below) with a set of symbols with known semantics, as described by a type instantiating this class.

(/.\) :: (a -> a') -> b a -> b a' infixl 4 Source #

Basic functor operator. Lifts a function (from a layer below) into the domain of the extended behavior layer.

(/*\) :: b (a -> a') -> b a -> b a' infixl 4 Source #

Applicative operator. Defines a resolution between two extended behavior symbols.

(/&\) :: b Bool -> b a -> b a infixl 4 Source #

Predicate operator. Generates a defined behavior based on an extended Boolean predicate.

(/!\) :: a -> b a -> a infixl 4 Source #

Degenerate operator. Degenerates a behavior-extended value into a non-extended one (from a layer below), based on a kernel value. Used also to throw exceptions.

Instances
ExB AbstExt Source #

Implements the absent semantics of the extended behavior atoms.

Instance details

Defined in ForSyDe.Atom.ExB.Absent

Methods

extend :: a -> AbstExt a Source #

(/.\) :: (a -> a') -> AbstExt a -> AbstExt a' Source #

(/*\) :: AbstExt (a -> a') -> AbstExt a -> AbstExt a' Source #

(/&\) :: AbstExt Bool -> AbstExt a -> AbstExt a Source #

(/!\) :: a -> AbstExt a -> a Source #

The Model of Computation (MoC) Layer

This layer represents a major part of the forsyde-atom library and is concerned in modeling the timing aspects of CPS. While its foundations have been laid in the classical ForSyDe [Sander04], it mainly tries to follow the tagged signal model [Lee98] as closely as it is permitted by the host language, and with the adaptations required by the atom approach.

Continuing the short description in <#package-header the introduction>, the following sections offer a short primer in ForSyDe-Atom and how it connects to the classical ForSyDe theory, culminating with an overview of the MoC layer as provided by forsyde-atom.

Signals

[Lee98] defines signals as ordered sets of events where each event is composed of a tag T and a value V, where T defines a total or partial order. Similarly, in ForSyDe a signal is defined as a sequence of events that enables processes to communicate and synchronize. Sequencing might infer an implicit total order of events, but more importantly it determines an order of evaluation, which is a key piece of the simulation engine.

In ForSyDe, sequencing is achieved using a Stream data type, inspired from [Reekie95]. In ForSyDe-Atom, signals are streams that carry events, where each type of event is identified by a type constructor. Hence the pseudo-Haskell definition for a signal would look like below, where e is the type of an event which encodes a tag system through its type constructor. Since, according to [Lee98], MoCs are defined by tag systems, we can state that any specific instance of a signal is describing (i.e. is bound to) a MoC.

type Signal a = exists e . MoC e => Stream (e a) 

data Stream e Source #

Defines a stream of events, encapsulating them in a structure isomorphic to an infinite list [Bird87], thus all properties of lists may also be applied to Streams. While, in combination with lazy evaluation, it is possible to create and simulate infinite signals, we need to ensure that the first/previous event is always fully evaluated. This can be translated into the following rule:

non-causal feedback
or "zero-delay" feedback loops are forbidden, due to un-evaluated self-referential calls. In a feedback loop, there always has to be enough events to ensure the data flow.

This rule imposes that the stream of data is uninterrupted in order to have an evaluatable kernel every time a new event is produced (i.e. to avoid deadlocks). Thus we can add the rule:

cleaning of output signals
through removing output events is also forbidden. In other words, for each new input at any instant in time, a process must react with at least one output event.

Constructors

NullS

terminates a signal

e :- (Stream e) infixr 3

the default constructor appends an event to the head of the stream

Instances
Functor Stream Source #

allows for the mapping of an arbitrary function (a -> b) upon all the events of a (Stream a).

Instance details

Defined in ForSyDe.Atom.MoC.Stream

Methods

fmap :: (a -> b) -> Stream a -> Stream b #

(<$) :: a -> Stream b -> Stream a #

Applicative Stream Source #

enables the Stream to behave like a ZipList

Instance details

Defined in ForSyDe.Atom.MoC.Stream

Methods

pure :: a -> Stream a #

(<*>) :: Stream (a -> b) -> Stream a -> Stream b #

liftA2 :: (a -> b -> c) -> Stream a -> Stream b -> Stream c #

(*>) :: Stream a -> Stream b -> Stream b #

(<*) :: Stream a -> Stream b -> Stream a #

Foldable Stream Source #

provides folding functions useful for implementing utilities, such as length.

Instance details

Defined in ForSyDe.Atom.MoC.Stream

Methods

fold :: Monoid m => Stream m -> m #

foldMap :: Monoid m => (a -> m) -> Stream a -> m #

foldr :: (a -> b -> b) -> b -> Stream a -> b #

foldr' :: (a -> b -> b) -> b -> Stream a -> b #

foldl :: (b -> a -> b) -> b -> Stream a -> b #

foldl' :: (b -> a -> b) -> b -> Stream a -> b #

foldr1 :: (a -> a -> a) -> Stream a -> a #

foldl1 :: (a -> a -> a) -> Stream a -> a #

toList :: Stream a -> [a] #

null :: Stream a -> Bool #

length :: Stream a -> Int #

elem :: Eq a => a -> Stream a -> Bool #

maximum :: Ord a => Stream a -> a #

minimum :: Ord a => Stream a -> a #

sum :: Num a => Stream a -> a #

product :: Num a => Stream a -> a #

Read a => Read (Stream a) Source #

signal (1 :- 2 :- NullS) is read using the string "{1,2}".

Instance details

Defined in ForSyDe.Atom.MoC.Stream

Show a => Show (Stream a) Source #

signal (1 :- 2 :- NullS) is represented as {1,2}.

Instance details

Defined in ForSyDe.Atom.MoC.Stream

Methods

showsPrec :: Int -> Stream a -> ShowS #

show :: Stream a -> String #

showList :: [Stream a] -> ShowS #

Plottable a => Plot (Signal a) Source #

SY signals.

Instance details

Defined in ForSyDe.Atom.Utility.Plot

Plottable a => Plot (Signal a) Source #

SDF signals.

Instance details

Defined in ForSyDe.Atom.Utility.Plot

Plottable a => Plot (Signal a) Source #

DE signals.

Instance details

Defined in ForSyDe.Atom.Utility.Plot

Plottable a => Plot (Signal a) Source #

CT signals.

Instance details

Defined in ForSyDe.Atom.Utility.Plot

For extended documentation and a list of all utilities associated with the Stream type you can consult:

Processes

As described in [Lee98], processes are either "set of possible behaviors" of signals or "relations" between multiple signals. One can describe complex systems by composing processes, which in this case is interpreted as the "intersection of the behaviors of each of the processes being involved". According to that framework, we can describe ForSyDe-Atom processes as having the following properties:

functionality
Processes are functional if provided they are stimulated with the same input signals, they react with the same output signals every time. This condition is fulfilled by Haskell's purity. On the other hand in the current modeling framework it is not possible to model non-functional processes.
determinancy
A functional process is determinate, which means that they describe either one behavior, or unambiguously no behavior.
strict causality
Refers to the fact that the distance between input signals of a process is strictly preserved at the output. This means that ForSyDe-Atom process networks are unable to describe and simulate delta-causal or non-causal systems (i.e. zero-delay feedback loops) in the MoC layer. These problems are solved in other layers (see [Ungureanu18])
monotonicity
In order to ensure causal order and determinancy, processes need to be monotonic. A signal's tags (if explicit) must be a partial or total order and all tag alterations must be monotonic.

ForSyDe inherits this definition with respect to a functional view, thus a process p is a functional mapping over (the history of) signals. A process can only be instantiated using a process constructor pc, which is a higher order function embedding MoC semantics and/or a specific composition, but lacking functionality. An intuitive way of viewing process constructors in general is as "parameterized templates" for processes. Stretching this analogy we take the liberty of referring to processes as "instances of process constructors".

In the definitions/figure above, \(v_i \in V\) may also denote the set of functions, not only values, fact which is taken for granted in Haskell. Actually the whole power of ForSyDe as a Haskell EDSL is that the designer can send functions as normal values in programs.

Since processes are functions, process composition is equivalent to function composition. This means that composing two processes p1 and p2 grants the process p2 . p1

p1      :: Signal α -> Signal β
p2      :: Signal β -> Signal γ
p2 . p1 :: Signal α -> Signal γ

This implies that there is a signal Signal β that "streams" the result from p1 to p2, as suggested in the drawing:

Process networks describe ForSyDe systems in terms of compositions of processes and originate from Reekie's process nets [Reekie95]. A process network is a process itself, i.e. function from signal(s) to signal(s). The composition above p2 . p1 can also be regarded as a process network.

In ForSyDe-Atom, MoC atoms are themselves process constructors, and follow the process constructor definition: they (may) take values as arguments and return processes. Based on that we can create the following equivalence table:

These equivalences fit well with intuition when considering how partial application and composition mechanisms are acting. The whole idea of atoms is basically applying Backus' principle of combining forms in order to obtain abstractions, which is one of the basic principles of the functional programming paradigm. To further even more this idea, one could visualize process networks as graphs, where processes are nodes and signals are edges. A subgraph with a meaningful shape could be considered a pattern (hence the name atom patterns), and one could find isomorphisms between different patterns.

To get a flavor of how (partial) composition of higher order function works in ForSyDe-Atom, consider the example below where both pn and p' denote the same thing and instantiate the pattern in the right hand side, visualized as a graph. The circled operators denote the -.- and -*- atoms presented in the next section.

Models of Computation

MoCs are classes of behaviors dictating the semantics of execution and concurrency in a network of processes and, according to [Lee98], are determined by the tag systems. Based on how their tag systems are defined ForSyDe identifies MoCs as:

  1. timed where T is a totally ordered set and, depending on the abstraction level, t might express from the notion of physical time (e.g. continuous time CT, discrete event DE) to the notion of precedence and causality (e.g. synchronous SY);
  2. untimed, where T is a partially ordered set and t is expressed in terms of constraints on the tags in signals (e.g. dataflow, synchronous data flow SDF).

As concerning MoCs, ForSyDe implements the execution semantics through process constructors, abstracting the timing model and inferring a schedule of the process network. Furthermore, processes are side-effect-free, ensuring the functional correctness of a system even from early design stages. In ForSyDe-Atom all instances of MoC atoms embed operating semantics dictated by a certain MoC.

Representing Time

Some MoCs require explicit time representation, for which forsyde-atom provides two distinct data types.

type Time = Rational Source #

Type alias for the type to represent metric (continuous) time. Underneath we use Rational that is able to represent any \(t\) between \(t_1 < t_2 \in T\).

type TimeStamp = DiffTime Source #

Alias for the type representing discrete time. It is inherently quantizable, the quantum being a picosecond ( \(10^{-12}\) seconds), thus it can be considered order-isomorphic with a set of integers, i.e. between any two timestamps there is a finite number of timestamps. Moreover, a timestamp can be easily translated into a rational number representing fractions of a second, so the conversion between timestamps (discrete time) and rationals (analog/continuous time) is straightforward.

This type is used in the explicit tags of the DE MoC (and subsequently the discrete event evaluation engine for simulating the CT MoC).

MoC Layer Overview

Now, after the crash course in ForSyDe, we can finally present what the MoC layer consists of. Similarly to all other layers, the MoC layer defines:

  • 4 atoms provided as infix operators and implemented as type class methods for the class MoC. Since each atom's semantics is overloaded based on the input type, and each input type defines an own tag system, we enforce Lee's idea <#lee98 [Lee98]> that tag systems determine the MoC (semantics). (See below)
  • a library of meaningful atom patterns as process constructors. (Check the ForSyDe.Atom.MoC module).
  • a set of data types representing events defining tag systems through their structure (i.e. T × V). These types are instances of the MoC type class and are defining the rules of execution which will trigger an atom to behave in accordance to an associated MoC. For each supported MoC, forsyde-atom provides a module which defines the signal type, but also a library of utilities and helpers for specific instantiations of atom patterns. (Check the instances).

class Applicative e => MoC e where Source #

This is a type class defining interfaces for the MoC layer atoms. Each model of computation exposes its tag system through a unique event type which is an instance of this class, defining \( T \times V \).

To express all possible MoCs which can be described using a tagged signal model we need to capture the most general form of their atoms. This means that under the same interface we need to describe atoms with different execution regimes. Recall that atoms are in principle applicative functors which act upon one input signal at a time and partially apply functions. Depending on the execution regime, these function might or might not need additional parameters to determine the behavior for evaluating each argument. These additional parameters we call, in loose terms, as the execution context.

execution context
Additional information which, paired with a function, completely determines the behavior of a MoC atom (i.e. process).

The left-hand side expression above shows the most general notation used to describe a function with n inputs of (possibly different) types \(\alpha\) and m outputs of (possibly different) types \(\beta\) executed in context \(\Gamma\). The right-hand side expression shows that in ForSyDe-Atom context is associated with each and every argument in order to enable the applicative mechanisms. Depending on the MoC, \(\breve\alpha\) would translate to:

One example of execution context is the consumption and production rates for data flow MoCs (e.g. SDF). In this case the passed functions are defined over "sequences" or "partitions" of events, i.e. groupings of events with the same partial order in relation to a process firing.

While in the example above the execution context can be extracted from the type information, working with type-level parameters is not a trivial task in Haskell, especially if we want to describe a general and extensible type class. This is why we have chosen a pragmatic approach in implementing the MoC class:

  • any (possible) Cartesian product which denotes a partition of \(\alpha\) is represented using a recursive type, namely a list \([\alpha]\).
  • as the execution context cannot (or can hardly) be extracted from the recursive type, in the most general case we pass both context and argument as a pair (see each instance in particular). To aid in pairing contexts with each argument in a function, the general purpose ctxt utilities are provided (see ctxt22).
  • this artifice is masked using the generic type families Fun and Ret.

Minimal complete definition

(-.-), (-*-), (-*), (-<-), (-&-)

Associated Types

type Fun e a b Source #

This is a type family alias \(^1\) for a context-bound function passed as an argument to a MoC atom. It can be regarded as an enhanced -> type operator, specific to each MoC.

\(^1\) While hiding the explicit definition of arguments, this implementation choice certainly has its advantages in avoiding unnecessary or redundant type constructors (see version 0.1.1 and prior). Aliases are replaced at compile time, thus not affecting run-time performance.

type Ret e b Source #

Like Fun, this alias hides a context-bound value (e.g. function return). This alias is needed for utilities to recreate clean types again (see -*).

Methods

(-.-) :: Fun e a b -> Stream (e a) -> Stream (e b) infixl 5 Source #

The func atom is mapping a function on values (in the presence of a context) to a signal, i.e. stream of tagged events. As ForSyDe deals with determinate, functional processes, this atom defines the (only) behavior of a process in rapport to one input signal [Lee98].

(-*-) :: Stream (e (Fun e a b)) -> Stream (e a) -> Stream (e b) infixl 5 Source #

The sync atom synchronizes two signals, one carrying functions on values (in the presence of a context), and the other containing values. During the synchronization it applies the function(s) carried by the former signal on the values carried by the latter. This atom defines a relation between two signals [Lee98].

(-*) :: Stream (e (Ret e b)) -> Stream (e b) infixl 3 Source #

Artificial utility which drops the context and/or partitioning yielding a clean signal type.

(-<-) :: Stream (e a) -> Stream (e a) -> Stream (e a) infixl 3 Source #

The pre atom prepends the prefix of the left signal operand (i.e. the first event in timed MoCs, or the first n events in untimed MoCs) at the beginning of the right signal operand \(^1\). This atom is necessary to ensure complete partial order of a signal and assures the least upper bound necessary for example in the evaluation of feedback loops [Lee98].

\(^1\) this atom acts like the pre operator in the synchronous language Lustre [Halbwachs91], and for timed MoCs it behaves the same. For untimed MoCs though, the length of the prefix of a signal is assumed to be the length of a signal, since the API does not provide any other means to pass n as a parameter.

(-&-) :: Stream (e a) -> Stream (e a) -> Stream (e a) infixl 3 Source #

The phi atom manipulates the tags in a signal in a restrictive way which preserves monotonicity and continuity in a process [Lee98], namely by “phase-shifting” all tags in a signal with the appropriate metric corresponding to each MoC. Thus it preserves the characteristic function intact [Sander04].

The metric unit used for phase shifting is inferred from the prefix of the left signal operand, while right signal operand is the one being manipulated.

Instances
MoC SY Source #

Implenents the execution semantics for the SY MoC atoms.

Instance details

Defined in ForSyDe.Atom.MoC.SY.Core

Associated Types

type Fun SY a b :: * Source #

type Ret SY b :: * Source #

Methods

(-.-) :: Fun SY a b -> Stream (SY a) -> Stream (SY b) Source #

(-*-) :: Stream (SY (Fun SY a b)) -> Stream (SY a) -> Stream (SY b) Source #

(-*) :: Stream (SY (Ret SY b)) -> Stream (SY b) Source #

(-<-) :: Stream (SY a) -> Stream (SY a) -> Stream (SY a) Source #

(-&-) :: Stream (SY a) -> Stream (SY a) -> Stream (SY a) Source #

MoC SDF Source #

Implenents the SDF semantics for the MoC atoms.

Instance details

Defined in ForSyDe.Atom.MoC.SDF.Core

Associated Types

type Fun SDF a b :: * Source #

type Ret SDF b :: * Source #

Methods

(-.-) :: Fun SDF a b -> Stream (SDF a) -> Stream (SDF b) Source #

(-*-) :: Stream (SDF (Fun SDF a b)) -> Stream (SDF a) -> Stream (SDF b) Source #

(-*) :: Stream (SDF (Ret SDF b)) -> Stream (SDF b) Source #

(-<-) :: Stream (SDF a) -> Stream (SDF a) -> Stream (SDF a) Source #

(-&-) :: Stream (SDF a) -> Stream (SDF a) -> Stream (SDF a) Source #

MoC DE Source #

Implenents the execution semantics for the DE MoC atoms.

Instance details

Defined in ForSyDe.Atom.MoC.DE.Core

Associated Types

type Fun DE a b :: * Source #

type Ret DE b :: * Source #

Methods

(-.-) :: Fun DE a b -> Stream (DE a) -> Stream (DE b) Source #

(-*-) :: Stream (DE (Fun DE a b)) -> Stream (DE a) -> Stream (DE b) Source #

(-*) :: Stream (DE (Ret DE b)) -> Stream (DE b) Source #

(-<-) :: Stream (DE a) -> Stream (DE a) -> Stream (DE a) Source #

(-&-) :: Stream (DE a) -> Stream (DE a) -> Stream (DE a) Source #

MoC CT Source #

Implenents the execution semantics for the CT MoC atoms.

Instance details

Defined in ForSyDe.Atom.MoC.CT.Core

Associated Types

type Fun CT a b :: * Source #

type Ret CT b :: * Source #

Methods

(-.-) :: Fun CT a b -> Stream (CT a) -> Stream (CT b) Source #

(-*-) :: Stream (CT (Fun CT a b)) -> Stream (CT a) -> Stream (CT b) Source #

(-*) :: Stream (CT (Ret CT b)) -> Stream (CT b) Source #

(-<-) :: Stream (CT a) -> Stream (CT a) -> Stream (CT a) Source #

(-&-) :: Stream (CT a) -> Stream (CT a) -> Stream (CT a) Source #

The Skeleton Layer

The skeleton layer describes recursive and regular composition of processes which expose inherent potential for parallelism. As such, it wraps lower layer entities (i.e. processes, signals), into regular structures called categorical types. Most of the ground work for this layer is based on the categorical type theory [Bird97], which enable the description of algorithmic skeletons as high-level constructs encapsulating parallelism and communication with an associated cost complexity.

This layer provides:

  • 3 atoms as infix operators which, as demonstrated in [Bird97] and [Skillicorn05], are enough to describe all algorithmic skeletons.
  • a library of generic skeletons as specific atom patterns. (Check the ForSyDe.Atom.Skeleton module).
  • a set of different categorical types which implement these atoms, as instances of the Skeleton type class. These types provide additional skeletons patterns of atoms which takes as arguments their own type constructors. (Check the instances).

class Functor c => Skeleton c where Source #

Class containing all the Skeleton layer atoms.

This class is instantiated by a set of categorical types, i.e. types which describe an inherent potential for being evaluated in parallel. Skeletons are patterns from this layer. When skeletons take as arguments entities from the MoC layer (i.e. processes), the results themselves are parallel process networks which describe systems with an inherent potential to be implemented on parallel platforms. All skeletons can be described as composition of the three atoms below (=<<= being just a specific instantiation of =\=). This possible due to an existing theorem in the categorical type theory, also called the Bird-Merteens formalism [Bird97]:

factorization
A function on a categorical type is an algorithmic skeleton (i.e. catamorphism) iff it can be represented in a factorized form, i.e. as a map composed with a reduce.

Consequently, most of the skeletons for the implemented categorical types are described in their factorized form, taking as arguments either:

  • type constructors or functions derived from type constructors
  • processes, i.e. MoC layer entities

Most of the ground-work on algorithmic skeletons on which this module is founded has been laid in [Bird97], [Skillicorn05] and it founds many of the frameworks collected in [Gorlatch03].

Minimal complete definition

(=.=), (=*=), (=\=)

Methods

(=.=) :: (a -> b) -> c a -> c b infixl 4 Source #

Atom which maps a function on each element of a structure (i.e. categorical type), defined as:

=.= together with =*= form the map pattern.

(=*=) :: c (a -> b) -> c a -> c b infixl 4 Source #

Atom which applies the functions contained by as structure (i.e. categorical type), on the elements of another structure, defined as:

=.= together with =*= form the map pattern.

(=\=) :: (a -> a -> a) -> c a -> a infixl 2 Source #

Atom which reduces a structure to an element based on an associative function, defined as:

(=<<=) infixl 2 Source #

Arguments

:: c (a -> a)

vector of functions

-> a

kernel element

-> a

result

Skeleton which pipes an element through all the functions contained by a structure.

N.B.: this is not an atom. It has an implicit definition which might be augmented by instances of this class to include edge cases.

As the composition operation is not associative, we cannot treat pipe as a true reduction. Alas, it can still be exploited in parallel since it exposes another type of parallelism: time parallelism.

first :: c a -> a Source #

Returns the first element in a structure.

N.B.: this is not an atom. It has an implicit definition which might be replaced by instances of this class with a more efficient implementation.

last :: c a -> a Source #

Returns the last element in a structure.

N.B.: this is not an atom. It has an implicit definition which might be replaced by instances of this class with a more efficient implementation.

Instances
Skeleton Vector Source #

Ensures that Vector is a structure associated with the Skeleton Layer.

Instance details

Defined in ForSyDe.Atom.Skeleton.Vector.Core

Methods

(=.=) :: (a -> b) -> Vector a -> Vector b Source #

(=*=) :: Vector (a -> b) -> Vector a -> Vector b Source #

(=\=) :: (a -> a -> a) -> Vector a -> a Source #

(=<<=) :: Vector (a -> a) -> a -> a Source #

first :: Vector a -> a Source #

last :: Vector a -> a Source #

Utilities

The ForSyDe.Atom module export a set of utility functions, mainly for helping to write more concise code or to perform regular chores like plotting, or nicer printouts.

The ForSyDe.Atom.Utility.Plot module contains utilities for dumping and visualizing the data in ForSyDe-Atom models in different formats, e.g. LaTeX or gnuplot.

The ForSyDe.Atom.Utility.Tuple library contains functions that help in avoiding working with explicitly zipping and unzipping structures of n-tuples. These utilities work mainly on the structures of data without altering the information, thus they are not considered atoms and are not associated with any layer.

Among the most useful of these utilities we mentions the unzip function. When consulting the ForSyDe-Atom papers or further checking the modules' API documentation, you will notice that in all our formal definitions, patterns are expressed in the most general form as functions from n-ary Cartesian products to m-ary Cartesian products. While partial application provides a versatile mechanism which translates n-ary inputs into curried arguments (which is a powerful mechanism in combination with an applicative style of programming), for the return types we must rely on tuples. But working with tuples of data wrapped in several layers of structures becomes extremely cumbersome. Take for example the case of a process constructed with pc in equation (1) below. Using only the atoms defined by MoC to implement pc we would be able to design a process which returns only one signal carrying tuples and not, as we would like, a tuple of signals.

Therefore, by implementing all data types associated with signals and events as instances of Functor, we were able to provide a (set of) unzip utility functions defined like in equation (2) above. Mind that we call unzip a utility and not an atom, since it has no behavioral semantic. It just conveniently un-wraps tuples and lifts them into layers above.

(||<) :: (Functor f1, Functor f2) => f1 (f2 (a1, a2)) -> (f1 (f2 a1), f1 (f2 a2)) infixl 3 Source #

This set of utility functions "unzip" nested n-tuples, provided as postfix operators. They are crucial for reconstructing data types from higher-order functions which input functions with multiple outputs. It relies on the nested types being instances of Functor.

The operator convention is (|+<+), where the number of | represent the number of layers the n-tuple is lifted, while the number of < + 1 is the order n of the n-tuple.

ForSyDe.Atom.Utility exports the constructors below. Please follow the examples in the source code if they do not suffice:

   |<,    |<<,    |<<<,    |<<<<,    |<<<<<,    |<<<<<<,    |<<<<<<<,    |<<<<<<<<,
  ||<,   ||<<,   ||<<<,   ||<<<<,   ||<<<<<,   ||<<<<<<,   ||<<<<<<<,   ||<<<<<<<<,
 |||<,  |||<<,  |||<<<,  |||<<<<,  |||<<<<<,  |||<<<<<<,  |||<<<<<<<,  |||<<<<<<<<,  
||||<, ||||<<, ||||<<<, ||||<<<<, ||||<<<<<, ||||<<<<<<, ||||<<<<<<<, ||||<<<<<<<<, 

Example:

>>> :set -XPostfixOperators
>>> ([Just (1,2,3), Nothing, Just (4,5,6)] ||<<)
([Just 1,Nothing,Just 4],[Just 2,Nothing,Just 5],[Just 3,Nothing,Just 6])

Bibliography

[Bird87] Bird, R. S. (1987). An introduction to the theory of lists. In Logic of programming and calculi of discrete design (pp. 5-42). Springer Berlin Heidelberg.

[Bird97] Bird, R. S. & de Moor, O. (1997). Algebra of Programming. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.

[Fujimoto00] Fujimoto, R. M. (2000). Parallel and distributed simulation systems (Vol. 300). New York: Wiley.

[Halbwachs91] Halbwachs, N., Caspi, P., Raymond, P., & Pilaud, D. (1991). The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79(9), 1305-1320.

[Gorlatch03] Fischer, J., Gorlatch, S., & Bischof, H. (2003). Foundations of data-parallel skeletons. In Patterns and skeletons for parallel and distributed computing (pp. 1-27). Springer London.

[Kahn76] Kahn, G., & MacQueen, D. (1976). Coroutines and networks of parallel processes.

[Lee98] Lee, E. A., & Sangiovanni-Vincentelli, A. (1998). A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12), 1217-1229.

[Reekie95] Reekie, H. J. (1995). Realtime signal processing: Dataflow, visual, and functional programming.

[Sander04] Sander, I., & Jantsch, A. (2004). System modeling and transformational design refinement in ForSyDe [formal system design]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 23(1), 17-32.

[Skillicorn05] Skillicorn, D. B. (2005). Foundations of parallel programming (No. 6). Cambridge University Press.

[Ungureanu17] Ungureanu, G., & Sander, I., A layered formal framework for modeling of cyber-physical systems, in 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pp. 1715–1720.

[Ungureanu18] Ungureanu, G., de Medeiros, J. E. G. & Sander, I., Bridging discrete and continuous time models with Atoms, in 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2018, pp. 277-280