Synchronous programming language: Difference between revisions

Revision as of 19:54, 23 September 2016

Revision as of 03:32, 2 January 2018

Line 10:

The synchronous abstraction makes reasoning about time in a synchronous program a lot easier, thanks to the notion of '''logical ticks''': a synchronous program reacts to its environment in a sequence of ticks, and computations within a tick are assumed to be instantaneous, i.e., as if the processor executing them were infinitely fast. The statement “'''a||b'''” is therefore abstracted as the package “'''ab'''” where “'''a'''” and “'''b'''” are simultaneous. To take a concrete example, the Esterel statement “'''every 60 second emit minute'''” specifies that the signal “'''minute'''” is exactly synchronous with the 60-th occurrence of the signal “'''second'''”. At a more fundamental level, the synchronous abstraction eliminates the non-determinism resulting from the interleaving of concurrent behaviors. This allows '''deterministic''' semantics, therefore making synchronous programs amenable to formal analysis, verification and certified code generation, and usable as formal specification formalisms.

In contrast, in the asynchronous model of computation, on a sequential processor, the statement “'''a||b'''” can be either implemented as "'''a;b'''" or as "'''b;a'''". This is known as the '''interleaving-based non determinism'''. The drawback with an asynchronous model is that it intrinsically forbids deterministic semantics (e.g., race conditions), which makes formal reasoning such as analysis and verification more complex. Nonetheless, asynchronous formalisms are very useful to model, design and verify distributed systems, because they are intrinsically asynchronous.

Also in contrast are systems with processes that basically ''interact synchronously''. An example would be systems built based on the [[Communicating sequential processes|Communicating sequential processes (CSP)]] model, which also allows nondeterministic choice.