Concurrent Goal-Based Execution of Constraint Handling Rules

We (my PhD student Edmund and me) have just submitted a paper with this title to Theory and Practice of Logic Programming. The paper complements our PPDP'08 paper on parallel Constraint Handling Rules execution. You can get the paper here.

Here's what the abstract says:
We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes.

Transactions in Constraint Handling Rules

A paper to be presented at ICLP'08, Udine, Italy, December'08. My co-author Tom Schrijvers will give the presentation but here's already a draft of the talk.

If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.

In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper.

Gossiping girls

In my class on UPPAAL (a modeling and analysis tool for communicating FAs aka CFAs), I gave the following (classic) exercise:

A number of girls initially know one distinct secret each. Each girl has access to a phone which can be used to call another girl to share their secrets. Each time two girls talk to each other they always exchange all secrets with each other (thus after the phone call they both know all secrets they knew together before the phone call). The girls can communicate only in pairs (no conference calls) but it is possible that different pairs of girls talk concurrently.

Sounds like fun, right? Before, I discuss a sample solution in UPPAAL, let's consider some alternative frameworks which we could use to code up the above problem.

Here's a solution using CHR (Constraint Handling Rules):

  Girl(name1,secrets1), Girl(name2,secrets2) <==> 
         newSecrets(secrets1,secrets1) | let s=shareSecrets(secrets1,secrets2)
                                         in Girl(name1,s)
                                            Girl(name2,s)

What about using Join-patterns extended with guards and synchronous method calls:

   Girl(name1,secrets1) & Girl(name,secrets2) = do 
                              secrets1 := secrets1 `union` secrets2
                              secrets2 := secrets2 `union` secrets2

Okay, so finally my UPPAAL solution. First, the declarations plus description. The actual CFA is displayed below.

// =========================
// == Global declarations ==

// We introduce two channels. First, I thought we can do with just
// one channel but then I believe things will get really messy.

chan call, call2;

// We assume that there are three secrets: one, two and three

// To pass secrets among girls we introduce three (global) variables, 
// one for each secret.
// The value 0 indicates that the secret is not present (ie known).
// The value 1 indicates that the secret is known.

int var_s1, var_s2, var_s3;

// The actual transmission of values is performed in two steps:
//  1. First the caller tranfers her secrets
//  2. Then, it's the callee's turn to transfer her secrets.
// We must guarantee that this step happens atomically between
// two parties. We can either (a) use the UPPAAL feature of
// committed locations or (b) we simply transmit the callers identity 
// which then the callee transmits back for verification. 
// Option (a) sounds too easy, almost cheating :),
// so we'll pursue option (b). 

// To transmit the callers identity, we'll need another "message-passing" variable.

int var_id;

// WARNING: We use here the initial_secret as a unique identifier
// which implies that we only supports girls which initially now
// a distinct secret.

// Please check the declarations of the girl template which
// describes the ideas and functionality of the CFA.

// =======================================
// == Declarations of the girl template ==

// Three variables to represent the girl's knowledge/status about
// the three secrets.

// We will initialize the variables when instantiating
// the girl template. The input parameter initial_secret
// refers to the secret that's initially known.

int s1, s2, s3;

// local variables to store the transmitted messages (secrets and caller id)

int in1, in2, in3, in_id;

// The first step of the girl CFA is to record (locally) the initially known
// secret. View as programming if-then-else statements using CFA transitions.
// If initial_secret == 1 then s1 = 1, s2 = 0, s3 = 0
// else and so on

// It gets interesting once we reach the "Start" state.
// In the first stage, we can either make a call, via "call!", or receive a call via "call?".
// In case we're the caller, we transmit our secrets and our identity (in form of the
// initial_secret). In case we're the receiver of the call, we're storing the
// transmitted values. Then, in the second stage, the roles switch and the caller 
// becomes the receive and vice versa. Notice the use of a different channel.
// This is to avoid that a caller of the first stage can interact with a receiver
// of the second stage. We yet need to check that the caller and receiver of the
// first stage are still the same for the second stage. We perform this check
// in state "Verify" by comparing the transmited identify with our own (the initial_secret).
// A point to note is that this check is only performed by the receiver
// of the second stage.
// States "Update_Secrets1" and "Update_Secrets2" then update the secrets after the
// exchange. The formula (x+y) - (x*y) evaluates to 1 or 0 for values 0 and 1.
// Sure, this could be done smarter using bit operations or simply using UPPAAL's
// C-style array.

// =========================
// == System declarations ==

girl1 = Girl(1);
girl2 = Girl(2);
girl3 = Girl(3);

// List one or more processes to be composed into a system.
system girl1, girl2, girl3;

And finally the CFA:
Girl

Get your own at Scribd or explore others:

So, which solution do you prefer? To be fair, UPPAAL is not meant for programming, it has its strength in analyzing CFAs via its expressive query language and model checker.