Compiling Constraint Handling Rules with Lazyand Concurrent Search Techniques
Martin Sulzmann and Edmund S. L. Lam
School of Computing, National University of Singapore
S16 Level 5, 3 Science Drive 2, Singapore 117543{sulzmann,lamsoonl}@comp.nus.edu.sg

Abstract. Constraint Handling Rules [5] (CHR) is a concurrent commitedchoice constraint programming language to describe transformations (rewritings) among multi-sets of constraints. One of the main CHR execution
tasks is to search for constraints from the store which match the constraints in the CHR rule head. In this paper, we demonstrate that lazinessand concurrency are highly useful features to implement this search task
efficiently.

1

Introduction

Constraint Handling Rules [5] (CHR) is a high level concurrent commitedchoice constraint programming language to describe transformations (rewritings) among multi-sets of constraints (atomic formulae). Originally, CHR was
designed to write incremental constraint solvers, but CHR is now used in a wide
range of other applications such as type system design and agent specification.
The semantics of CHR and its compilation is a fairly well studied subject. [2,7, 10] Traditionally, CHR are compiled into logic languages such as Prolog and
HAL and a number of efficient implementations exist. CHR is also implemented
in Java [1] as well as the functional programming language Haskell [4]. One of themain compilation tasks is to search for constraints from the store which matchthe constraints in the CHR rule head.
In this paper, we demonstrate that laziness and concurrency are highly usefulfeatures to implement this search task efficiently. Lazy evaluation is the techniqueof delaying computations until the time where the result of the computation isrequired, thus allowing us to define operations like building the match tree ina purely declarative manner, without the worry of any runtime performance
penalties. Concurrency on the other hand allow us to specify search tasks inparallel, hence possibly improving the performance of CHR execution. For thispaper, we demostrate an implementation of the lazy and concurrent CHR matchsearching in Haskell [6], which is a lazy functional programming language withpowerful concurrency abstractions [9].
Specifically, we make the following contributions:– We first show how laziness can be used to implement the task of searchingfor matching constraints declaratively and thus more elegantly (Section 4).
Existing CHR optimizations such as optimal join ordering and early guardscheduling can be easily integrated into our approach.

– Next, we employ concurrency to implement the search task more efficiently(Section 5). As in the previous case, existing CHR optimization methods canbe integrated easily.
– We also develop a hybrid approach which combines laziness and concurrency(Section 6).
– We review a number of practical CHR examples which benefit from ourapproach (Section 7).
We continue in Section 2 where we highlight the key ideas of our lazy searchmethod. Section 3 reviews background material on CHR. We conclude in Section
8 where we also discuss related work.

2

A Motivating Example

A CHR program is essentially a set of rules that describes rewritings among a
multiset of constraints (atomic formulae) until a fixed-point is reached. A simple
example of a CHR program isA, B, C ⇔ D

A, B, C ⇒ D

A \ B, C ⇔ DThis example shows the three main types of CHR rules. The first rule isa simplification rule which says ”if constraints A,B and C are in the store,
then delete them and add D” while the second (middle), a propagation rulesays ”if constraints A,B and C are in the store, then add D”. The right mostrule is known as a simpagation rule which is a mix between simplification andpropagation rules: Constraints before the ’\’ (A) are not deleted, while constraint
after (B and C) are. Hence a significant part of CHR execution is the searchingfor sets of constraints in a constraint store that match rule heads (left-handside of rules). Particularly propagation rules need all possible matches, while
simplification rules only one. This search space can be abstractly viewed as amatch tree, which is an n-ary tree where each node contain a numbered constraint(constraints paired with unique integers to distinguish multiple copies) from theconstraint store. For instance, given the following constraint store S,
S ≡ {A#1, B#2, B#3, C#4, C#5}
we have a search space represented by the following match tree, assumingthat we search in a left to right ordering of the rule heads:
A#1
.

&

&

.

B#2
.
C#4
↓
M1

B#3
C#5
↓
M2

C#4
↓
M3

&
C#5
↓
M4

With lazy functional programming, we can implement the search for matching constraints elegantly as follows:2

data Cons = A | B | C | D
data MTree = MTree Cons [MTree]buildMTree :: [Cons] -> [Cons] -> [MTree]buildMTree (c:cs) store =let candidates = filter (==c) store
in map (\c’ -> MTree c’ (buildMTree cs store)) candidates
buildMTree [] = []propMatches :: [MTree] -> [[Cons]]
propMatches ((MTree c mts’):mts) =(map (c:) (propMatches mts’)) ++ (propMatches mts)
propMatches [] = []simpMatch :: [MTree] -> [Cons]
simpMatch mts = head (propMatches mts)

Functions propMatches and simpMatch are essentially defined by the samecode. The first argument (store) represents the constraint store, while thesecond represents the left hand side of the rule. Lazy evaluation ensures thatwhen findOneMatch is called, only the first match is evaluated, thus never suffers from unneccessary runtime computations of unrequired matches. Note thatlazy evaluation also allow us to separately define the search space construction buildMTree and the searching routines declaratively without performance
penalty. The matching tree may seem redundant here when defined only for simplification and propagation matches, however when we introduce simpagation
rule matches (Section 4.2), where an efficient implementation involves pruning
techniques, its purpose will be more significant.
We have made a few simplifying assumptions in the above framework: First,
constraints are just propositional, hence matching here is simple equality. Also,
CHR rules traditionally include guard conditions which must be checked before
a match can be commited. We will address these extensions Section 4.

3

Constraint Handling Rules

3.1

Syntax and Semantics

We review the syntax and refined operational semantics of CHR. CHR describes
multi-set rewriting of constraints, which are either builtin constraints or CHR
constraints. These rewritings are specified by a set of CHR simpagation rules ofthe form:r @ H1 \ H2 ⇔ g | C
We call H1 the propagation heads and H2 the simplification heads of therule, each of which are sequences of CHR constraints. g is a builtin constraint
referred to as the guard and C, a sequence of CHR and builtin constraints isthe body of the rule. We assign each constraint in H1 and H2 a unique integer,
known as the occurrence number. We shall denote a simpagation rule with empty
propagation head (simplification rule) as r @ H ⇔ C and a simpagation rulewith empty simplification head (propagation rule) as r @ H ⇒ C. We denote3the empty list as  and the empty set as ∅. Multiset union is denoted by ] andwe sometimes treat sequences (lists) as multisets if ordering is unimportant.
To differentiate among copies of the same CHR constraints in the multiset
store, we introduce numbered CHR constraint, which is a CHR constraint cpaired with an integer n denoted by c#n. We will refer to this integer n as
the identifier of the constraint c. For convinence, we define auxiliary functionsCons(c#n) and Id(c#n) which returns c and n respectively, and overload themto lists and multisets of constraints in the obvious manner. A CHR execution
state is the tuple:hG, S, B, T in
where G is a multiset of constraints known as the goals, S is a multiset of
CHR constraints (constraint store), B is a builtin constraint builtin store, T
is the propagation history which is a set of sequences of constraint identifiers
appended with a rule name. Finally, n is an integer representing the next free
identifier.
Informally the refined CHR semantics defines the exhaustive application of
CHR rules, triggered by a multiset of goal constraints. The declarative semantics
is based on the following 3 transitions, which maps execution states to execution
states C to C 0 , denoted C  C 0 .
hG, S, B, T in  hG, S, B, T in
1. Solveh{b} ] G, S, B, T in  hG, S, b ∧ B, T in
where b is a built-in constraint.
2. Introduceh{c} ] G, S, B, T in  hG, {c#n} ] S, B, T i(n+1)
where c is a CHR constraint.
3. ApplyhG, H1 ] H2 ] S, B, T in  hθ(C) ] G, H1 ] S, B, T 0 in
where∃(r @ H10 \ H20 ⇔ g | C) ∧∃θ, a matching substitution such that:
Cons(H1 ) ≡ θ(H10 )Cons(H2 ) ≡ θ(H20 )CT |=S B → ∃r (θ ∧ g)
Id(H1 ) + +Id(H2 ) + +[r] ∈/TT 0 ≡ {Id(H1 ) + +Id(H2 ) + +[r]} ∪ T

The Solve transition passes a new built-in constraint to the built-in store,
while the Introduce transition does the same for CHR constraints to the constraint store. The Apply transition non-deterministically picks a rule and asubset of the constraint store that contains constraints matching the heads ofthe rule and applies the rewrite specified by the rule, provided the guard is entailed from the constraint theory CT . The history list T keeps track of all rule
combinations that has fired, so as to ensure that each set of constraints matchinga rule head fires a rule at most once.
The declarative semantics is highly non-deterministic. This is because it
declaratively specifies the operational behaviour of CHR programs, but do not4impose explicitly an order in which goals are processed and an order in which rulematches are tried. Most CHR systems implement the refined operational semantics [3] which defines a more deterministic execution model of CHR programs.
Informally, the refined semantics execute CHR goals in left-to-right depth firstorder, which essentially means treating the goals G of a CHR execution state as a
stack: only the left most constraint (active) may be executed for any given state,
and newly added constraints are added to the left (head) of G. Further more,an active goal constraint must be matched with rule heads in a specific order,
normally assumed to be the top down and left-to-right order of appearence of the
CHR rule heads. Note that the matching tree abstraction is also compatible withthe refined semantics, simply by only allowing match trees to be construction
from the active goal constraint as the root.
Consider the abstract CHR program shown in Figure 1 which consists of 3
rules: r1 is a simplification rule (no propagate heads), r2 a propagation rule (nosimplify heads) and r3 a simpagation rule. The following shows a constraint store
S from the CHR program in figure 1, and a corresponding match tree containing
matching heads of the r3 rule under the active constraint a(5, W ).
Constraint Store S
S ≡ {a(5, R)#1, c(R, 3)#2, c(R, 2)#3, b(2)#4, b(8)#5}
Match Tree of r3 @ a(X, Y ) \ b(W ), c(Y, Z) ⇔ X > Z | d(X, W, Y, Z)
P rop a(X, Y ) :a(5, R)#1.
&
Simp c(Y, Z) :c(R, 3)#2
c(R, 2)#4.
&.
&
Simp b(W ) : b(2)#5
b(8)#6 b(2)#5
b(8)#6↓↓↓↓
M atch :
θ1
θ2
θ3
θ4
where θ1 ≡ {X 7→ 5, Y 7→ R, Z 7→ 3, W 7→ 2}θ3 ≡ {X 7→ 5, Y 7→ R, Z 7→ 2, W 7→ 2}θ2 ≡ {X 7→ 5, Y 7→ R, Z 7→ 3, W 7→ 8}
θ4 ≡ {X 7→ 5, Y 7→ R, Z 7→ 2, W 7→ 8}

We assume for now that the order in which partner constraints are searched
for is arbitrally chosen. In practice, optimal join ordering is determined by analysis techniques detailed in [2]. A CHR rule head match is a pair consisting of aset of matching constraints and the matching substitution that matches it to the
CHR rule head. Note that for the above matching tree, we will fire the matches{(θ1 , {#1, #2, #5}), (θ4 , {#1, #4, #6})} as each contains their own unique simplification heads ({#2, #5} and {#4, #6} respectively). Another alternative setof matches that may fire is {(θ2 , {#1, #2, #6}), (θ3 , {#1, #4, #5})}. If we consider the simplification rule r1 instead we can only fire a single match, while in
the other extreme case (propagation rule r2), we can fire all matches (assumingthat none has been fired before).

4

Searching For Matching Constraints Lazily

We refine the approach from Section 2 to handle the full CHR semantics, by
including matching substitutions and guard constraints. First, we consider the5

r1 @ a(X, Y ), b(W ), c(Y, Z) ⇔ X > Z | d(X, W, Y, Z)
r2 @ a(X, Y ), b(W ), c(Y, Z) ⇒ X > Z | d(X, W, Y, Z)
r3 @ a(X, Y ) \ b(W ), c(Y, Z) ⇔ X > Z | d(X, W, Y, Z)
Fig. 1. An Example CHR Program

data Term
data Cons= Value String | Var String= Cons { symbol::String , args::[Term] }| NumCons { nsymbol::String , nargs::[Term] , nid::Int }data RuleHead = RuleHead { htype::HeadType , cons::Cons }data HeadType = Simp | Prop
type Subst= [(Term,Term)]
apply:: Subst -> Cons -> Cons
compose :: Subst -> Subst -> Subst
match:: Cons -> Cons -> Maybe Subst

Fig. 2. CHR Data Representation & Matching Interfaces

special cases of simplification and propagation CHR in Section 4.1. As observed
earlier, in case of a simplification CHR we only require to find one match whereas
for a propagation CHR we want to find all matches. The situation gets more
complicated in case of simpagation CHR rules, which we will address in Section
4.2.
Figure 2 shows the representation of terms and constraints in Haskell datatypes Term and Cons. The RuleHead and RuleType datatypes describe ruleheads, which are essentially constraints tagged with a head type indicating if
it is a simplification Simp or propagation Prop head. These are followed by interfaces of substitution and matching over terms and constraints in 3 functions
apply, compose and match with their obvious meanings. An occurrence rule headcompilation is thus represented by a list of RuleHead datatypes.
4.1

Lazy Simplification and Propagation Match Search

We show now how simplification (one match) and propagation matches (allmatches) can be implemented lazily. Figure 3 shows the matching tree data structure MTree and a naive implementation of the CHR constraint store ListCHRStore,
which is simply a list of constraints. The function getCandidates retrieves all
matching constraints from a constraint store given the constraint to be matched.
The SearchTask data type represents the matching search sequence for each
CHR rule occurrence. A search task Lookup c represents the task of branching
the search with constraints in the store matching c, while Guard g means thatthe guard g can be schedule at the current node (hence pruning away nodes that
do not pass the guard). Hence for a CHR rule r @ A, B, C ⇒ g | D, we assume
that its head and guard is compiled into 3 basic matching search sequence (as6

type ListCHRStore
data MTree= [Cons]= MNode RuleHead [MTree] | MLeaf Subst

getCandidates :: Cons -> ListCHRStore -> [(Subst,Cons)]
getCandidates p (c:cs) =case match p c ofJust sub -> (sub,c):(getCandidates p cs)
Nothing -> getCandidates p cs
getCandidates [] = []data SearchTask = Lookup RuleHead| Guard (Subst -> Bool)buildMTree :: Subst -> [SearchTask] -> ListCHRStore -> [MTree]buildMTree sub ((Guard g):ts) st =if g sub then buildMTree sub ts st else []buildMTree sub ((Lookup r):ts) st =let RuleHead h c = r
ms = getCandidates (apply sub c) st
in map (\(sub’,c’) -> MTree (RuleHead h c’) (buildMTree (compose sub sub’) ts st)) ms
buildMTree sub [] = [MLeaf sub]data Match = Match { subst::Subst , heads::[RuleHead] }propMatches :: [RuleHead] -> [MTree] -> [Match]
propMatches rs ((MNode r mts’):mts) = (propMatches (rs++[r]) mts’)++(propMatches rs mts)
propMatches rs ((MLeaf sub):mts) = (Match sub rs):(propMatches rs mts)
propMatches [] = []simpMatch :: [RuleHead] -> [MTree] -> Match
simpMatch rs mts = head (propMatches rs mts)

Fig. 3. MTree Builder & Simplification/Propagation Rule Head Match Searchsuming left to right ordering of rule heads), one for the search sequence startingfrom each rule head occurrence:occurrenceA ≡ [Lookup A, Lookup B, Lookup C, Guard g]
occurrenceB ≡ [Lookup B, Lookup A, Lookup C, Guard g]
occurrenceC ≡ [Lookup C, Lookup A, Lookup B, Guard g]

This compilation scheme of CHR rule heads is almost similiar to existing
schemes. Note that basic CHR optimizations [7, 2, 10] can be applied to thiscompilation. The function buildMTree returns all possible matching trees given
a constraint store and a list of SearchTask. Note that we can use the refinedsemantics to ’drive’ the search by supplying an active constraint as the root ofa MTree. An important point is that the buildMTree declaratively specifies theentire match tree that represent the search space of finding rule head matchesfrom a constraint store. However, in a lazy language like Haskell subtrees of the7data TVar a
newTVar:: STM (TVar a)
readTVar :: TVar a -> STM awriteTVaratomically:: TVar a -> a -> STM ():: STM a -> IO a

Fig. 4. Haskell Transactional Memory Interfaces

mtree are only ever computed when their values are explicitly required. Thisapplies also to the getCandidate function.
The data type Match represents a match pair consisting of matching substitution of type Subst and the set of matching rule heads of type [RuleHead].
Given a list of MTree, propagation and simplification matches can be extracted
by the the propMatches (returns all matches from a MTree) and simpMatch(returns left most match from a MTree) functions. The simpMatch function isdefined as the head (left most) element of the result of propMatches and thanks
to laziness, the tail of the list is never evaluated.
4.2

Lazy Simpagation Match Search

Simplification and propagation are special cases where we must retrieve one or
all of the matches, tasks which requires no search. In this section we show how anefficient match search routine for simpagation rules can be implemented. Since,
the former rules can be treated as special simpagation rules, this implementation
subsumes that of the previous subsection. Consider the following matching tree,
from the example in Section 3.1:
P rop a(X, Y ) :a(5, R)#1

Simp c(Y, Z) :M atch :&&.

c(R, 3)#2.

Simp b(W ) :.

b(2)#5↓θ1c(R, 2)#4
b(8)#6↓
θ2b(2)#5↓
θ3&b(8)#6↓
θ4

We wish to find the matches {(θ1 , {#1, #2, #5}), (θ4 , {#1, #4, #6})} as theyeach have unique simplification heads. A naive way to do this is to extract allmatches and linear filter away overlapping matches. However we wish to do
this efficiently, by pruning away overlapping matches in the MTree. Note thatcommiting to θ1 not only invalidates θ2 (a sibling), it also invalidates θ3 (nonsibling). Hence to prune away invalidate matches, we can ’thread’ through a listof constraints (possibly indexed by constraint id) representing the constraints
which already has been commited. This solution however introduce the additional burden of keeping track of and indexing a simplification head ’history’list.
A better solution would be to allow the search procedures to immediately
physically commit to the match (delete simplification heads from the constraint
store) after verifying that all its simplification heads are still in the store. If
8simplification heads cannot be verified (already deleted), the match is dropped.
Thus we do not need to keep track of any additional data structures, while
the match search procedure additionally contains the side-effects of deleting
simplification head constraints from the store (a task which must anyway bedone during execution of CHR). However, representing the store as a pure list
ListCHRStote and the pure functions in Figure 3 do not allow us to specify side
effects in Haskell. Thus we look to monads and mutable references in Haskell.
Monads provides the Haskell programmer a mechanism to define operations withside-effects, as well as an interface to define imperative style operations. The key
idea of monads is as follows: a type of IO a where IO is a monad, represents
an IO operation that performs some action (which may contain side-effects) andproduces a value of type a.
Figure 4 shows the interface for the TVar data type which is a mutable transactional memory reference and some monadic operations. A type TVar a is areference to a value of type a. newTVar, readTVar and writeTVar provides creation, read and write interfaces to transaction memory. Note that transactional
memory operations are executed only on the STM monad. The atomically operation simply executes an STM operation as an IO operation. For reasons that will
be clearer in the next section (Section 5) we have chosen to use transactional
memory as our store references. However, for the purpose of this section, it issuffice to treat TVar’s as standard mutable reference. Monads also introduces
strictness (as oppose to laziness), hence by default a monadic operation IO a
must be executed in an imperative sequence. However, the Haskell libraries doprovide primitives to allow programmers to write non-strict monadic operations.
For instance, we can write a lazy map IO monad operation as follows:
mapIOLazily :: (a -> IO b) -> [a] -> IO [b]mapIOLazily f (a:as) = do b <- f abs <- unsafeInterleaveIO (mapIOLazily f as)
return (b:bs)
mapIOLazily [] = return []The unsafeInterleaveIO :: IO a → IO a library operation takes an IO
action of type IO a, but delays the execution of this action until the value of ais required. Figure 5 illustrates the interfaces of an implementation of the CHRStore on shared memory. For brevity we only show the interfaces of the reference
CHR store with the assumption that CHR store is implemented on transactional
memory. getCandidatesIO and buildMTreeIO are the monadic versions of theMTree building operations. Note that we define them lazily with the help of theunsafeInterleaveIO operation. removeAllOrNone, whose purpose will be clear
soon, is an STM operation which works as follows: check that a given list of
constraints is in the shared store and if so remove all from the store and return
true, otherwise just return false.
Figure 6 shows the simpagateMatchesIO operation which implements thesearch for matches with non-overlapping simplification heads. It is summarized
by the following: If the current node is an MNode search it only if the constraint it
represents is still in store, by returning one match (simplification) or all matches(propagation). If it is an MLeaf, delete all simplification heads from the store
and return the match. Note that deleteAllOrNone seemingly would never failand always return true. However, this is not true when we consider a concurrent
search technique (Section 6).
9data RefCHRStore
deleteFromStore:: SharedCHRStore -> Cons -> STM ()isStored:: SharedCHRStore -> Cons -> STM Bool
getStoredContents :: SharedCHRStore -> STM [Cons]
getCandidatesIO :: Cons -> SharedCHRStore -> IO [(Subst,Cons)]
getCandidatesIO c st = dols <- getStoredContents st
return (getCandidates c ls)
buildMTree :: Subst -> [SearchTask] -> ListCHRStore -> [MTree]buildMTree sub ((Guard g):ts) st =if g sub then buildMTree sub ts st else []buildMTree sub ((Lookup r):ts) st =let RuleHead h c = r
ms = getCandidates (apply sub c) st
in map (\(sub’,c’) -> MTree (RuleHead h c’) (buildMTree (compose sub sub’) ts st)) ms
buildMTree sub [] = [MLeaf sub]buildMTreeIO :: Subst -> [SearckTask] -> RefCHRStore -> IO [MTree]buildMTreeIO sub ((Guard g):ts) st = docase g sub ofTrue-> buildMTreeIO sub ts st
False -> return [] buildMTreeIO sub ((Lookup r):rs) st = dolet RuleHead h c = r
ms <- getCandidatesIO (apply sub c) st
mapIOLazily (buildMTreeIO’ sub r rs st) ms
where
buildMTreeIO’ sub (RuleHead h c) rs st (sub’,c’) = do
mts <- buildMTreeIO (compose sub sub’) rs st
return (MTree (RuleHead h c’) mts)
buildMTreeIO sub [] = return [MLeaf sub]removeAllOrNone :: RefCHRStore -> [Cons] -> STM BoolremoveAllOrNone st cs = dobs <- mapM (isStored st) cs
case and bs ofTrue-> do deleteFromStore st cs
return True
False -> return False

Fig. 5. Shared CHR Store & Monadic MTree Operations

5

Searching for Matching Constraints Concurrently

The previous section highlights the lazy approach of implementing CHR simpagation rule head matching. The match search function is essentially a tree
search algorithm through the MTree, hence it is possible and beneficial to search
10simpagateMatchesIO :: [RuleHead] -> RefCHRStore -> [MTree] -> IO [Match]
simpagateMatchesIO rs st ((MNode r mts):mts’) = doisvalid <- atomically (isStored st (cons r))
if isvalid then do
mcs <- simpagateMatchesIO (rs++[r]) st mts
mcs’ <- unsafeInterleaveIO (simpagateMatchesIO rs st mts’)case (htype r) of
Simp -> do case mcs of(m: ) -> return (m:mcs’)[]-> return mcs’
Prop -> return (mcs++mcs’)
else simpagateMatchesIO rs st mts’)simpagateMatchesIO rs st ((MLeaf sub):mts) = dolet simpheads = map cons (filter ((==Simp).htype) rs)
succ <- atomically (deleteAllOrNone st simpheads)
if succ then do
mcs <- unsafeInterleaveIO (simpagateMatchesIO rs st mts)
return ((Match sub rs):mcs)
else simpagateMatchesIO rs st mts)
simpagateMatchesIO[] = return []Fig. 6. Simpagation Rule Head Match Searchingdata TChan a
newTChan:: STM (TChan a)
readTChan:: TChan a -> STM awriteTChan :: TChan a -> a -> STM ()forkIO:: IO () -> IO ThreadId

Fig. 7. Transactional Channels & IO Forking Operation

branches of the tree concurrently. In this section, we present an alternative tothe lazy match search of Section 4: concurrent matching searching.
Up to now, we have only used the STM transaction memory as standard mutable memory references. Yet in fact the STM monad actually provides a Haskell
programmer a concurrency abstraction that supports composable operations andcommunication channels TChan between concurrent processes. Show in Figure 7,
a TChan act as a channel of communication, which can be created, read and written into by the operations newTChan, readTChan and writeTChan. Recall that
STM operations are executed from the IO monad with operation atomically(Figure 4). This execution of an STM operation is guaranteed to be atomic (Anoperation is fully executed as a single atomic action) and isolated (Effects of an
uncompleted operation cannot be observed by other concurrent operations, until
it has completed/commited).
Figure 8 shows a brute force implementation of the concurrent match search.
The concSimpagateMatchIO operation computes a set of non-overlapping matches
the brute force way: fork an IO thread for every branch of the MTree. Matches are
11

concSimpagateMatchIO :: [MTree] -> SharedCHRStore -> IO (TChan Match)
concSimpagateMatchIO mts st = do
ms <- atomically newTChan
mapM (\mt -> forkIO (concSimpagateMatchIO’ [] ms st mt)) mts
return ms
where
concSimpagateMatchIO’ :: [RuleHead] -> TChan Match -> SharedCHRStore -> MTree -> IO ()concSimpagateMatchIO’ rs tms st (MNode r mts) = doisvalid <- atomically (isStored st (cons r))
if isvalid then do
mapM (\mt -> forkIO (concSimpagateMatchIO’ (rs++[r]) tms st mt)) mts
else return ()concSimpagateMatchIO’ rs tms st (MLeaf sub) = dolet simpheads = map cons (filter ((==Simp).htype) rs)
succ <- atomically (removeAllOrNone st simpheads)
if succ then do
atomically (writeTChan tms (Match sub rs))
else return ()Fig. 8. Brute Force Concurrent Match Searchgathered into a signal transactional channel which is returned as the final result.
Each thread independently determine if their correspond match do not conflictwith any other, simply by atomically verifying (removeAllOrNone) that theirsimplification heads have not been removed from the store and removing them if
verification is successful. If this atomic operation is a success, the corresponding
matching data can be placed in the transactional channel.

6

Lazy and Concurrent Match Search

The concurrent match search discuss in Section 5 effectively computes the entire
MTree, ignoring any possible pruning of matches. This may mean that we will
eventually compute many redundant matches, for instance only a single matchis ever possible from a sub-tree with simplification root but the search of thissub-tree is still done by mutliple competing threads.
This can be highly inefficient at times and the concurrent match searchingroutine should be less aggressive when spawning threads to search sub-trees
rooted by simplification nodes. The are several design decisions we can choose,
one of which is to set a trashhold value for maximum number of threads for eachbranches once the search reach its first simplification node. A more interesting
and balanced search strategy is to combine the lazy and concurrent search strategy, where concurrent search is performed up to the first simplification headfrom the top.
We provide, in Figure 9, the lazy and concurrent match search implementation in Haskell. Note that it prunes simplification nodes by executing a lazysearch (simpagateMatchesIO of Figure 6) in place of the concurrent search. Also
note that now the purpose of using STM transactional memory for the lazy search
12lconcSimpagateMatchIO :: [MTree] -> SharedCHRStore -> IO (TChan Match)lconcSimpagateMatchIO mts st = do
ms <- atomically newTChan
mapM (\mt -> forkIO (lconcSimpagateMatchIO’ [] ms st mt)) mts
return ms
wherelconcSimpagateMatchIO’ :: [RuleHead] -> TChan Match -> SharedCHRStore -> MTree -> IO ()lconcSimpagateMatchIO’ rs tms st (MNode r mts) = doisvalid <- atomically (isStored st (cons r))
if isvalid then docase (htype r) of
Simp -> do ms <- simpagateMatchesIO rs st [MNode r mts]
atomically (writeTChan tms (head ms))
Prop -> mapM (\mt -> forkIO (lconcSimpagateMatchIO’ (rs++[r]) tms st mt)) mts
else return ()lconcSimpagateMatchIO’ rs tms st (MLeaf sub) = dolet simpheads = map cons (filter ((==Simp).htype) rs)
succ <- atomically (removeAllOrNone st simpheads)
if succ then do
atomically (writeTChan tms (Match sub rs))
else return ()Fig. 9. Lazy and Concurrent Match Search Implementation

is clear as it allows us to integrated the lazy search with the concurrent search
consistently (Using standard Haskell mutable memory (MVars) would not allow
us to safely compose these two operations).

7

Practical Examples

In this section, we show some examples of actual CHR programs that may benefit
from the lazy and concurrent search match strategy. Consider Greatest Common
Divisor (GCD) CHR program with the initial store S
gcd1 @ gcd(0) ⇔ T rue
gcd2 @ gcd(n) \ gcd(m) ⇔ m > n | gcd(m − n)S ≡ {gcd(2)#1, gcd(3)#2, gcd(4)#3, gcd(5)#4, }Suppose we build a match tree for the second Gcd rule, with gcd(2)#1 as
the root matching with the propagation head gcd(n):13P rop gcd(n) :.
Simp gcd(m) :M atch :gcd(3)#2↓
θ1where θ1 ≡ {n 7→ 2, m 7→ 3},

gcd(2)#2↓&
gcd(4)#3
gcd(5)#4↓↓
θ2
θ3

θ2 ≡ {n 7→ 2, m 7→ 4},θ3 ≡ {n 7→ 2, m 7→ 5}

The concurrent match search would spawn a thread for each branch to thesimplfication heads matching gcd(m), hence three variants of rule gcd2 can fireconcurrently.
Next, consider the CHR program modelling an Authorized Access Only
Buffer Protocol. Agents are allowed to execute two actions get(Id, X) and put(Id, X)
to get and put integers into a shared channel chan(Ch, Ids). However get andput actions of respective agents are only possible if it is authorized to access thechannel.
get @ chan(Ch, Ids) \ get(Id, X), buf (Ch, Y ) ⇔ Id ∈ Ids | X = Y
put @ chan(Ch, Ids) \ put(Id, X) ⇔ Id ∈ Ids | buf (Ch, X)
S ≡ { chan(c1, [a1, a2])#1, get(a1, M )#2, get(a3, N )#3, get(a2, P )#4,
buf (c1, 1)#5, buf (c1, 2)#6, ...., buf (c1, 100)#104}

The store S consist of a single channel c1 which agents a1 and a2 has access,3 get actions and 100 integers. Consider the match tree of the get rule withchan(c1, [a1, a2])#1 as the root. We assume that the lazy and concurrent searchstrategy and early guard scheduling analysis has scheduled the guard Id ∈ Ids
right after the get(Id, X) head matches are retrieved.
P rop chan(Ch, Ids) :.
Simp get(Id, X) :Simp buf (Ch, Y ) :M atch :get(a1, M )#2↓
buf (c1, 1)#5↓
θ1chan(c1, [a1, a2])#1↓&
get(a3, N )#3
get(a2, P )#4↓&
buf (c1, 1)#5
buf (c1, 2)#6↓
θ2where θ1 ≡ {Ch 7→ c1, Ids 7→ [a1, a2], Id 7→ a1, X 7→ M, Y 7→ 1}θ2 ≡ {Ch 7→ c1, Ids 7→ [a1, a2], Id 7→ a2, X 7→ P, Y 7→ 2}

The above shows the sub-tree explored by the lazy and concurrent searchstrategy. Concurrent search is executed at the top level, hence the propagation
node chan(Ch, Ids) spawns a thread for each constraint matching get(Id, X).
Since the next nodes are simplification heads, lazy searches are executed fromthat point. This decision turns out to be a good one, since a brute force concurrent search would unneccessarily compute a match for each buffer and get action
pairs, most of which have over-lapping simplification heads.
14

8

Conclusion and Related Works

We have highlighted the implementation of two search techniques for CHR rulehead matching, namely lazy and concurrent search, which is compatiable withstandard CHR compilation optimization techniques. Lazy evaluation allows us
to define search routines declaratively while not forcing strict and unnecessary
runtime computations. Concurrent searching allows us to explore the search
space of rule head matches more efficiently. By combining the two approaches,
we have a more well-balanced and practical search strategy.
Optimized CHR compilation techniques have been widely studied. An implementation of CHR in Haskell is also explored in [4]. CHR match search compilations discussed in [2] follows a strict order of processing CHR constraints
similiar to Prolog style (left-to-right, depth first) evaluations, while our implementation is more closely related to [10] which allows multiple rule variants tofire from active constraints matching propagation rule heads. Yet to the best of
our knowledge, we are the first to explicitly explore concurrent and lazy matchsearch techniques. Local optimization techniques like optimal join-ordering andearly guard scheduling discussed in [7, 2, 10] are compatible with our implementation.
In future, we intend to introduce these match searching techniques to our concurrent CHR implementation [8]. Other possible future works include integratingother existing CHR optimization techniques (eg. late storage, continuation optimizations, etc) into our frame work, as well as obtaining emprical results on theperformance of various match search techniques discussed here.

References
1. K.
u.
leuvenjava
constraint
handling
rules(jchr)
system.
http://www.cs.kuleuven.ac.be/˜ dtai/projects/CHR.
2. G. J. Duck. Compilation of Constraint Handling Rules. PhD thesis, The Universityof Melbourne, 2005.
3. G. J. Duck, P. J. Stuckey, M. J. Garcı́a de la Banda, and C. Holzbaur. The Refined
Operational Semantics of Constraint Handling Rules. In Proc of ICLP’04, volume3132 of LNCS, pages 90–104. Springer-Verlag, 2004.
4. Gregory J. Duck. Haskell chr. http://www.cs.mu.oz.au/ gjd/haskellchr/.
5. T. Frühwirth. Theory and practice of constraint handling rules. Journal of Logic
Programming, Special Issue on Constraint Logic Programming, 37(1-3):95–138,
1998.
6. Haskell home page. http://www.haskell.org/.
7. C. Holzbaur, M. J. Garcı́a de la Banda, P. J. Stuckey, and G. J. Duck. Optimizing
compilation of Constraint Handling Rules in HAL. TPLP, 5(4-5):503–531, 2005.
8. E. S. L. Lam and M. Sulzmann. A concurrent Constraint Handling Rules implementation in Haskell with software transactional memory, 2007. Proc. of ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP’07).
9. S. Peyton Jones, A. Gordon, and S. Finne. Concurrent Haskell. In Proc. of
POPL’96, pages 295–308. ACM Press, 1996.
10. T. Schrijvers. Analyses, optimizations and extensions of Constraint HandlingRules: Ph.D. summary. In Proc. of ICLP’05, volume 3668 of LNCS, pages 435–436.
Springer-Verlag, 2005.

15