Mathematical Semantics for FBP - Graph Theory

photopin cc

In search of descriptive and inferential semantics for FBP.

TL;DR In trying to develop mathematical semantics for FBP, in order to reason about FBP programs and design experiments to test hypotheses, it is proposed that Graph Theory (GT) can describe the properties and behaviours of an FBP program. Which is nice.

The value of defining mathematically based compliance design criteria for libfbp is that such a definition could serve as a standard. Such a precise specification for any FBP implementation informs the programmer using it that they can rely on certain axiomatic behaviours and, being a modular programming paradigm, be assured of the reliable conjunction of FBP modules from widely differing sources. 

Beyond its immediate utility then, developing mathematical semantics for libfbp/FBP at an early stage will hopefully forestall problems with the quality of libfbp programs—as Brookes states[1] 

“Clearly, no program can be more reliable than the implementation of the language in which it is expressed for input to a computer.”

The benefits to FBP go beyond quality issues and extend to the potential for the formal proof of correctness for a libfbp program. Given that each libfbp component is in, and as of, itself an isolated Von-Neumann machine, then Hoare-style logics for sequential languages based on state-transformation semantics are particularly suited to the way a component functions. 

In this way the modular approach to building a FBP program provides islands of correctness communicating via connections. Subsequently, and given proof of conformity with the mathematical model, FBP developers have powerful mathematical tools at their disposal to formally prove correctness. 

The question then arises as to what mathematical semantics are most appropriate for describing libfbp program structure or rather its form?

A CSP approach to FBP inter-component communication

photopin cc

Any portal in a storm!

TL;DR Sometimes maligned, C++ multiple inheritance allows an object to be 2 things at once—such as both an input port and an output port. In this way any would-be-component class that multiply descends from both fbp::input and fbp::output port classes has the is-a-relationship that enables it to be connected to any other so descended component. Neat huh?

It is axiomatic in Hoare's CSP theory[1][2][3] that the internal states of a Component are invisible to its environment and communication between processes can only take place at one of two unidirectional input and output channels. Most common variants[4] of CSP approach the two channel restriction problem by describing communication at multiple named unidirectional channels such that each CSP event m.t consists of two  parts: m the channel name and t the message content. Thus for a process that engages in event t via channel m and then behaves as process P is denoted:

m.t -> m.P

In order for libfbp to be CSP compliant then, the only communication that an fbp::component can engage in is via its named input and output ports. Assuming it is possible to build any functional FBP program using libfbp  then there is no reason that CSP compliance should be sacrificed, and with it the opportunity to use process calculus to prove program correctness. With this goal of CSP compliance in mind, what then is the best way to implement port only based communication?

Compile-Time Brittle Run-Time Robust Static Type Safe FBP Connections

photopin cc

A bit of C++ untyped-to-typed separation template magic...

TL;DR You can have your cake and eat it! With collections of non-typed connectable classes static_cast to the typed template connection<T> interface opens up a world of ways of connecting together components!

The design decision to construct libfbp as a strictly type safe implementation of FBP is primarily aimed ensuring that no operation leads to undefined behaviour. 

Unfortunately there is an implementation dichotomy between being able to create a typed first-class FBP connection object and freely pass around such connections as the arguments in generic functions that manage those connections or the collections that store them.

A CSP approach to FBP Information Packets

What exactly are we delivering here?

TL;DR Don't look now the CSP event is the FBP IP, the FBP IP is the std::unique_ptr.

The real world has put a significant crimp on my programming of late but I have had plenty of time to think about things, so this post is rather theory heavy and code light.

The axiomatic processes of CSP Theory have been implemented as FBP Components here, here and here; but what of the FBP Information Packet (IP) - does it have a CSP equivalent?

A CSP approach to FBP Components: #3 RUN the livelock component #4 CHAOS the unpredictable component

Just because you're doing something doesn't mean everything is going well!

TL;DR The CSP process RUN represents livelock[1] and the entirely unpredictable mix of livelock and/or deadlock[2] is represented by the CHAOS process. Despite the difficulty in detecting these 2 worse case scenarios they are embodied as libfbp components.

The distributed deadlocked component that is failing to progress can be detected[2] by limiting the amount of time that a component will tolerate failing to progress. A much harder situation detect is one of livelock where a component will engage in any Information Package (IP) without making any meaningful progress. Harder still to detect is that chaotic component which can either engage in any IP or refuse to engage in any IP - it is in a superposition of livelock and deadlock!

A CSP approach to FBP Components: #2 SKIP success component.

Successful termination.

TL;DR  The next primitive CSP process to emulate in libfbp is SKIP for successful termination.

Given that the theory of Communicating Sequential Processes (CSP) is not a programming language but rather a mathematical notation for process algebra, nevertheless, there are a number of concurrent programming languages based on CSP; for example occam and Ada .

A CSP approach to FBP Components: #1 STOP the broken component.

Handling the broken component.

TL;DR FBP originates from the unashamedly pragmatic narrative tradition of software development and, consequently, lacks any mathematical semantics. The Theory of CSP is proposed not only as mathematical semantics for FBP but also a basis for its design and implementation. (Which I discuss at length in my Masters Thesis.)

As previously discussed here, it is clear that FBP falls into the Message Passing Model (MPM) of concurrency models. Further, message passing between isolated processes is a rudimentary description of not only FBP but also of Sir Tony Hoare's Communicating Sequential Processes (CSP)[1].