Pi4 - Applicability of pi-calculus to BCM "linking and switching" and V3

ebsoa message

Subject: Pi4 - Applicability of pi-calculus to BCM "linking and switching" and V3.0 ebBP?

I'm currently developing webservice software that is highly event/action driven and seeing several of the same issues regarding process timings, resource and coordination. Since its only a small local system - its solvable by traditional control logic.

SR-T - If you have a livelock, a race condition, or a deadlock, it will show up as either a warning or an error in your system description, and it will point you to the specific lines in your choreography where that's occurring. You won't have to be aware how it does that. What you'll get is, 'Hey, you might have a problem here."

SS So in much the same way that the compiler would have flagged a low-level error in days gone by, this will flag an error in the interactions modeling.

"That's how we can manage to engage with the widest community in terms of furthering the groundbreaking work. Just to give you an example, we've got Kohei Honda, Nobuko Yoshida, and Robin Milner all working on the open source stuff for the advanced type system. We've also had two other research groups approach Pi4 Tech to contribute. One is the University of Bologna, which is well known in the pi-calculus community, and the other is Imperial College, which is Howard Foster's group that has been using something called the labeled transition system analyzer.

By open sourcing in this way, we've managed to remove all of the IP (intellectual property) issues that worry academics, and as a result, we have academia working on business-focused problems, which is very rare. I know that Professor Robin Milner is very excited by the way we've managed to pull people together and to give relevance to all the body of work that he has founded, and it's that relevance that's key".

Being able to detect these issues at the compiler / runtime level - is something I'm used to using in Prolog - where it will explicitly warn you that something is non-deterministic.

We already have the means in BPSS to leverage Prolog-style deterministic logic checks ( Yes - you implicitly want business agreements to be deterministic and therefore legal!!!).

But - introducing the BCM notion of linking-and-switching - and a control agent for that - does mean that now its not possible for the local logic check to know if race conditions and other conflicts existing at the level of the whole network.

I know this is something that is not immediate for us - since BCM and BPSS are right now moving thru the "let's get this version out there and finished" mode - but once we circle back around in a month or so - to moving to "what's next" - this definately looks of potential applicability...