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 .
Therefore, theoretical results derived using the mathematical semantics of CSP are applicable to real-world programming. Further, taking forward the proposition that since FBP & CSP are both fundamentally Message Passing Models (MPMs) with disjoint local states then, CSP is applicable to the design and application of an FBP implementation.
Lemma 1: The CSP process can be mapped to the FBP component as an otherwise environmentally immune disjointed local state.
Therefore, the design decisions and their implementation for libfbp need not be arbitrary but, rather, be motivated by the concepts of CSP to enable not only the description but also ultimately simplify the process of proving the correctness of a libfbp program.
As discussed for the stop component previously, within CSP it is the process that is the behaviour pattern of an object, wherein the behaviour is described by the reaction to an occurrence or event e.g. (in CSP process algebra notation)
(pizza -> LETS_EAT)
With the simplest CSP process of STOP in hand as the libfbp component stop - the component which represents deadlocked behaviour. The next CSP process primitive is SKIP which, axiomatically, does nothing but terminate successfully by responding to success event (however that occurrence may be defined):
(success -> SKIP)
or idiomatically for CSP success is often denoted ✓ the termination event.
(✓ -> SKIP)
In order to have the potential to behave as the STOP process the skip component must subclass the stop component. However, as the libfbp class hierarchy develops it is clear that only the skip component should subclass stop - for without this any component could subclass stop and would slice off the ability to successfully terminate!
Thus, the first job is to hide the stop constructor from public view and befriend skip component:
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "component.h" | |
#include "fbp_deadlock_exception.h" | |
namespace fbp { | |
template<typename T> | |
class skip; //need anonymous reference in order to avoid ciruclar dependencies between stop.h and skip.h | |
template<typename T> | |
class stop: public component<T> { | |
friend class skip<T>; //befriend skip so that it alone may subclass via the private constructor | |
stop(T& enqueuer): component<T>(enqueuer) {} //private construcotr | |
protected: | |
virtual void do_run() override { | |
throw fbp_deadlock_exception(doh::FAIL + doh::FBP_STOP); //same behaviour | |
} | |
}; | |
} |
With which the skip component can now alone use stop as its parent class:
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "stop.h" | |
namespace fbp { | |
template<typename T> | |
struct skip: public stop<T> { | |
skip(T& enqueuer): stop<T>(enqueuer) {} | |
protected: | |
virtual void do_run() override { | |
this->terminate(); //component base class behvaiour | |
delete this; //this will do for now | |
} | |
}; | |
} |
The behaviour for successful termination described is to render the component terminated (taking itself out of the execution queue) and then delete itself from the free store. Clearly, such self deleting behaviour is risk prone as it requires that the component was constructed in the free store with new() in the first place[1,2,3] but at this stage it will suffice without overcomplicating this class with template policy behaviours.
Usage of skip is as per stop and is hopefully intuitive:
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class some_child_component { | |
protected: | |
virtual void do_run() { | |
. | |
. | |
. | |
//some mechanism to detect success ✓ | |
skip::do_run() //behave as the SKIP component | |
} | |
}; |
So, that's a couple of ways to terminate but what about actually doing something?
Well I'm going to take that question and RUN with it next time...
References:
No comments:
Post a Comment