The foreign function interface (FFI) present in the latest beta releases of LuaJIT is really nice for when you need to do things outside the Lua world. At runtime you pass it some C function definitions, and then everything you've defined becomes callable, and these calls are subsequently JIT compiled in the most efficient way possible. For example, we can define and then call some Windows API functions:

ffi = require "ffi"
ffi.cdef [[
  typedef void* HWND;
  HWND FindWindowA(const char* lpClassName, const char* lpWindowName);
  int GetWindowTextA(HWND hWnd, char* lpString, int nMaxCount); ]]
len = 300
buffer = ffi.new("char[?]", len)
window = ffi.C.FindWindowA("Notepad++", nil)
len = ffi.C.GetWindowTextA(window, buffer, len)
print(ffi.string(buffer, len)) --> C:\Lua\ffi_example.lua - Notepad++

This is fine and dandy for calling C from Lua, but things get rather more complicated with callbacks from C back to Lua. For example, the Windows EnumChildWindows function accepts a callback, which gets calls for every child of the given window. LuaJIT will happily accept and understand the definition of this function:

ffi.cdef [[
  typedef void* HWND;
  typedef bool (*WNDENUMPROC)(HWND, long);
  bool EnumChildWindows(HWND hWndParent, WNDENUMPROC lpEnumFunc, long lParam); ]]

You quickly run into a problem if you try to call it though, as you realise that the LuaJIT FFI currently lacks support for turning Lua functions into something which can called from C. At this point, most people would acknowledge that the FFI isn't yet complete, and then go to write their own C glue around EnumChildWindows using the traditional (slow) Lua C API. On the other hand, if you're feeling foolhardy, then you can fight the FFI to get callbacks working, and do so without resorting to any external C code. Naturally, this is what we'll do.

Our strategy will be to perform some control flow contortions so that when EnumChildWindows calls the callback, it infact returns to Lua, then Lua calls back to resume the enumeration. If we could write it in Lua, then it might look something like:

EnumChildWindows = coroutine.wrap(function()
  while true do
    ffi.C.EnumChildWindows(coroutine.yield(), function(hWnd)
      coroutine.yield(hWnd)
    end, nil)
  end
end)

Naturally we cannot write this in Lua, but we can write it in machine code, and we can then use the FFI to load and execute machine code. The coroutine trickery will be done by the Windows fiber API, as fibers are fairly similar to coroutines.

To start with, ConvertThreadToFiber can be called to convert the currently running thread into a fiber and return the handle to the fiber. Though if the thread is already a fiber then we run into a problem, as GetCurrentFiber is a macro rather than a function, and hence is not callable by the FFI. For now we'll ignore this issue, but it will be addressed later. Next we can call VirtualAlloc to allocate some executable memory, use ffi.copy to copy some machine code into said executable memory, then call the equivalent of coroutine.wrap, which is CreateFiber. In code, this looks like:

ffi.cdef [[
  void* ConvertThreadToFiber(void* lpParameter);
  typedef void (*LPFIBER_START_ROUTINE)(void*);
  void* CreateFiber(size_t dwStackSize, LPFIBER_START_ROUTINE lpStartAddress, void* lpParameter);
  void* VirtualAlloc(void* lpAddress, size_t dwSize, uint32_t flAllocationType, uint32_t flProtect); ]]
our_fiber = ffi.C.ConvertThreadToFiber(nil)
machine_code = "TODO"
procs = ffi.C.VirtualAlloc(nil, #machine_code + 1, 0x3000, 0x40)
ffi.copy(procs, machine_code)
contortion_fiber = ffi.C.CreateFiber(1024, ffi.cast("LPFIBER_START_ROUTINE", procs), nil)

The next task is to replace the TODO with the machine code equivalent of the following pseudo-C:

for(;;) {
  EnumChildWindows(coroutine.yield(), EnumerationProcedure, 0);
}

BOOL EnumerationProcedure(HWND hWnd, void* lpParam) {
  coroutine.yield(hWnd);
  return TRUE;
}

First of all we need to make the pseudo-C slightly more C-like. In particular, the above still uses a hypothetical coroutine.yield. The fiber API presents a SwitchToFiber function, which differs from coroutine.yield in that it doesn't support parameters or return values, and it requires telling which fiber to switch to. We thus end up with something like:

void* our_fiber; // The result of ConvertThreadToFiber.
void* transfer_slot[2]; // To yield a value, put the value in [0] and a non-NULL value in [1].
                        // To yield nothing, put anything in [0] and NULL in [1].
for(;;) {
  EnumChildWindows(transfer_slot[0], enum_proc, 0);
  transfer_slot[1] = NULL;
  SwitchToFiber(our_fiber);
}

BOOL EnumerationProcedure(HWND hWnd, void* lpParam) {
  transfer_slot[0] = hWnd;
  SwitchToFiber(our_fiber);
  return TRUE;
}

Next we need to convert this down to assembly code, firstly for x86:

fiber_proc:
push 0
push enum_proc
mov eax, dword ptr [transfer_slot]
push eax
call EnumChildWindows
mov dword ptr [transfer_slot + 4], 0
push our_fiber
call SwitchToFiber
jmp fiber_proc

enum_proc:
mov eax, dword ptr [esp+4]
mov dword ptr [transfer_slot + 4], eax
push our_fiber
call SwitchToFiber
mov eax, 1
retn 8

And secondly for x64:

fiber_proc:
sub rsp, 28h
after_prologue:
mov rcx, qword ptr [rip->transfer_slot]
lea rdx, qword ptr [rip->enum_proc]
call qword ptr [rip->EnumChildWindows]
mov qword ptr [rip->transfer_slot + 8], 0
mov rcx, qword ptr [rip->our_fiber]
call qword ptr [rip->SwitchToFiber]
jmp after_prologue

enum_proc:
sub rsp, 28h
mov qword ptr [rip->transfer_slot], rcx
mov rcx, qword ptr [rip->our_fiber]
call qword ptr [rip->SwitchToFiber]
mov rax, 1
add rsp, 28h
ret

transfer_slot:    dq
                  dq
EnumChildWindows: dq
our_fiber:        dq
SwitchToFiber:    dq

At this point, we return to our earlier problem of GetCurrentFiber being a macro, and note that it boils down to the following assembly code, firstly for x86:

mov eax, dword ptr fs:[10h]
ret

And similarly for x64:

mov rax, qword ptr gs:[20h]
ret

Now we can convert the assembly down to machine code, and put everything together:

local ffi = require "ffi"
-- The definitions we want to use.
ffi.cdef [[
  typedef void* HWND;
  typedef bool (*WNDENUMPROC)(HWND, long);
  bool EnumChildWindows(HWND hWndParent, WNDENUMPROC lpEnumFunc, long lParam);
  int GetWindowTextA(HWND hWnd, char* lpString, int nMaxCount); ]]
-- Extra definitions we need for performing contortions with fibers.
ffi.cdef [[
  void* ConvertThreadToFiber(void* lpParameter);
  void SwitchToFiber(void* lpFiber);
  typedef void (*LPFIBER_START_ROUTINE)(void*);
  void* CreateFiber(size_t dwStackSize, LPFIBER_START_ROUTINE lpStartAddress, void* lpParameter);
  uint32_t GetLastError(void);
  void* VirtualAlloc(void* lpAddress, size_t dwSize, uint32_t flAllocationType, uint32_t flProtect);
  bool RtlAddFunctionTable(void* FunctionTable, uint32_t EntryCount, void* BaseAddress); ]]

local EnumChildWindows
do
  local GetLastError = ffi.C.GetLastError
  local contortion_fiber
  local procs
  local transfer_slot
  local init_callbacks
  if ffi.arch == "x86" then
    init_callbacks = function()
      -- Ensure that the thread is a fiber, converting if required.
      local our_fiber = ffi.C.ConvertThreadToFiber(nil)
      if our_fiber == nil and GetLastError() ~= 1280 then
        error("Unable to convert thread to fiber")
      end
      transfer_slot = ffi.new("void*[2]")
      -- fiber_proc: for(;;) {
      --               EnumChildWindows(transfer_slot[0], enum_proc, 0);
      --               transfer_slot[1] = 0; // to mark end of iteration
      --               SwitchToFiber(our_fiber);
      --             }
      local asm = "\x6A\x00" -- push 0
               .. "\x68????" -- push ????
               .. "\xA1????\x50" -- mov eax, dword ptr [????], push eax
               .. "\xE8????" -- call ????
               .. "\xC7\x05????\x00\x00\x00\x00" -- mov dword ptr [????], 0
               .. "\x68????" -- push ????
               .. "\xE8????" -- call ????
               .. "\xEB\xD8" -- jmp $-40
      -- enum_proc: transfer_slot[0] = *(esp+4); // the HWND
      --            SwitchToFiber(our_fiber);
      --            return TRUE;
               .. "\x8B\x44\x24\x04" -- mov eax, dword ptr [esp+4]
               .. "\x3E\xA3????" -- mov dword ptr [????], eax
               .. "\x68????" -- push ????
               .. "\xE8????" -- call ????
               .. "\x33\xC0\x40" -- mov eax, 1
               .. "\xC2\x08" -- retn 8 (*)
      procs = ffi.C.VirtualAlloc(nil, #asm + 1, 0x3000, 0x40)
      if our_fiber == nil then
        -- GetCurrentFiber()
        ffi.copy(procs, "\x64\xA1\x10\x00\x00\x00\xC3") -- return __readfsdword(0x10)
        our_fiber = ffi.cast("void*(*)(void)", procs)()
      end
      ffi.copy(procs, asm)
      local function fixup(offset, ptr, isrelative)
        local dst = ffi.cast("char*", procs) + offset
        ptr = ffi.cast("char*", ptr)
        if isrelative then
          ptr = ffi.cast("char*", ptr - (dst + 4))
        end
        ffi.cast("char**", dst)[0] = ptr
      end
      fixup( 3, ffi.cast("char*", procs) + 40)
      fixup( 8, transfer_slot)
      fixup(14, ffi.C.EnumChildWindows, true)
      fixup(20, transfer_slot + 1)
      fixup(29, our_fiber)
      fixup(34, ffi.C.SwitchToFiber, true)
      fixup(46, transfer_slot)
      fixup(51, our_fiber)
      fixup(56, ffi.C.SwitchToFiber, true)
      contortion_fiber = ffi.C.CreateFiber(1024, ffi.cast("LPFIBER_START_ROUTINE", procs), nil)
      init_callbacks = function() end
    end
  elseif ffi.arch == "x64" then
    init_callbacks = function()
      -- Ensure that the thread is a fiber, converting if required.
      local our_fiber = ffi.C.ConvertThreadToFiber(nil)
      if our_fiber == nil and GetLastError() ~= 1280 then
        error("Unable to convert thread to fiber")
      end
      -- fiber_proc: for(;;) {
      --               EnumChildWindows(transfer_slot[0], enum_proc, 0);
      --               transfer_slot[1] = 0; // to mark end of iteration
      --               SwitchToFiber(our_fiber);
      --             }
      local asm = "\x48\x83\xEC\x28" -- sub rsp, 28h
               .. "\x48\x8B\x0D\x75\x00\x00\x00" -- mov rcx, [rip->transfer_slot_0]
               .. "\x48\x8D\x15\x26\x00\x00\x00" -- lea rdx, [rip->enum_proc]
               .. "\x48\xFF\x15\x77\x00\x00\x00" -- call [rip->EnumChildWindows]
               .. "\x48\xC7\x05\x64\x00\x00\x00\x00\x00\x00\x00" -- mov [rip->transfer_slot_1], 0
               .. "\x48\x8B\x0D\x6D\x00\x00\x00" -- mov rcx, [rip->our_fiber]
               .. "\x48\xFF\x15\x6E\x00\x00\x00" -- call [rip->SwitchToFiber]
               .. "\xEB\xD9" -- jmp $-48
               .. "\x90\x90\x90\x90" -- pad 8
      -- enum_proc: transfer_slot[0] = rcx; // the HWND
      --            SwitchToFiber(our_fiber);
      --            return TRUE;
               .. "\x48\x83\xEC\x28" -- sub rsp, 28h
               .. "\x48\x89\x0D\x3D\x00\x00\x00" -- mov [rip->transfer_slot_0], rcx
               .. "\x48\x8B\x0D\x4E\x00\x00\x00" -- mov rcx, [rip->our_fiber]
               .. "\x48\xFF\x15\x4F\x00\x00\x00" -- call [rip->SwitchToFiber]
               .. "\x48\xC7\xC0\x01\x00\x00\x00" -- mov rax, 1
               .. "\x48\x83\xC4\x28" -- add rsp, 28h
               .. "\xC3" -- ret
               .. "\x90\x90\x90" -- pad 8
      -- unwind data
               .. "\0\0\0\0\52\0\0\0\120\0\0\0"
               .. "\56\0\0\0\93\0\0\0\120\0\0\0"
               .. "\1\4\1\0\4\66"
               -- pad 8
      -- mutable data
               -- transfer_slot_0
               -- transfer_slot_1
               -- EnumChildWindows
               -- our_fiber
               -- SwitchToFiber
      procs = ffi.C.VirtualAlloc(nil, #asm + 42, 0x103000, 0x40)
      if our_fiber == nil then
        -- GetCurrentFiber()
        ffi.copy(procs, "\x65\x48\x8B\x04\x25\x20\x00\x00\x00\xC3") -- return __readgsqword(0x20)
        our_fiber = ffi.cast("void*(*)(void)", procs)()
      end
      ffi.copy(procs, asm)
      transfer_slot = ffi.cast("void**", ffi.cast("char*", procs) + 128)
      transfer_slot[2] = ffi.cast("void*", ffi.C.EnumChildWindows)
      transfer_slot[3] = ffi.cast("void*", our_fiber)
      transfer_slot[4] = ffi.cast("void*", ffi.C.SwitchToFiber)
      ffi.C.RtlAddFunctionTable(ffi.cast("void*", ffi.cast("char*", procs) + 96), 2, procs)
      contortion_fiber = ffi.C.CreateFiber(1024, ffi.cast("LPFIBER_START_ROUTINE", procs), nil)
      init_callbacks = function() end
    end
  else
    error("Only x86 and x64 are supported")
  end
  EnumChildWindows = function(wnd)
    init_callbacks()
    transfer_slot[0] = wnd
    transfer_slot[1] = ffi.cast("void*", 1)
    local results = {}
    while true do
      ffi.C.SwitchToFiber(contortion_fiber)
      if transfer_slot[1] == nil then
        return results
      else
        results[#results + 1] = transfer_slot[0]
      end
    end
  end
end

With this mass of heavy complicated machinery in place, we can finally perform our original goal of enumerating windows:

local buffer  = ffi.new("char[?]", 300)
for _, window in ipairs(EnumChildWindows(nil)) do
  local len = ffi.C.GetWindowTextA(window, buffer, 300)
  if len ~= 0 then
    print(ffi.string(buffer, len))
  end
end

I freely admit that this solution isn't at all elegant, but it does show that callbacks are possible with the current LuaJIT FFI, without the need of resorting to additional C libraries.

I rent two virtual private servers, of which one is in the UK, and the other is in the USA. Recently I concluded that I was paying too much for my UK VPS, so I switched providers, which meant a change of location from London to Manchester, along with a change of IP address. During the migration, I decided that I didn't particularly like the authoritative DNS server I was running (PowerDNS), and so I decided to write my own authoritative DNS server. This caused the migration process to be rather longer than I expected; it changed from a few hours to about a week, but the end result was much more knowledge of the DNS protocol, a new side project, and a DNS sever which I'm happy with. Also, in the past few hours, my USA VPS migrated from Atlanta to Dallas due to my hosting provider wanting to phase out their presence in Atlanta, and this migration also carried with it a change of IP address. This migration was fairly quick and painless due to most of it being an automated process on the part of my hosting provider. The fact that the migration was quick was also helped by the fact that the VPS was already running my self written DNS server, and thus didn't prompt me into a new project.

Perhaps at some point in the future I'll finish extending this DNS server code, and actually publish it.

As often happens when I decide to revise Haksell, I've written a Brainfuck interpreter. This time around, there is better error handling, an optimisation stage, and a main procedure.

import IO
import System.Environment

-- Parser
type Cell = Int
type LineNum = Int
data Token = Leftward | Rightward | Plus Cell | In | Out | Loop [Token]
type Parsed = ([Token], String, LineNum)

parseChars :: String -> LineNum -> Parsed
parseChars [] l = ([], [], l)
parseChars (c:s) l = parseChar c s l
parseChar :: Char -> String -> LineNum -> Parsed
parseChar '<' = parseChar' Leftward
parseChar '>' = parseChar' Rightward
parseChar '+' = parseChar' (Plus 1)
parseChar '-' = parseChar' (Plus (-1))
parseChar ',' = parseChar' In
parseChar '.' = parseChar' Out
parseChar '[' =
  \s l -> let (ts, s', l') = parseChars s l in
    if null s' then
      error("Unmatched [ on line " ++ show l)
    else
      parseChar' (Loop ts) (tail s') l'
parseChar ']' = \s l -> ([], ']':s, l)
parseChar '\n' = \s l -> parseChars s (l + 1)
parseChar _ = parseChars
parseChar' :: Token -> String -> LineNum -> Parsed
parseChar' t s l = (t:ts, s', l') where (ts, s', l') = parseChars s l
parse :: String -> [Token]
parse s =
  if null s' then
    ts
  else
    error ("Unmatched ] on line " ++ show l)
  where (ts, s', l) = parseChars s 1

-- Optimiser
optimise :: [Token] -> [Token]
optimise ((Plus n):(Plus m):ts) = optimise ((Plus (n+m)):ts)
optimise ((Loop t):(Loop _):ts) = optimise ((Loop t):ts)
optimise (Leftward:Rightward:ts) = optimise ts
optimise (Rightward:Leftward:ts) = optimise ts
optimise ((Plus 0):ts) = optimise ts
optimise ((Loop t):ts) = (Loop (optimise t)):(optimise ts)
optimise (t:ts) = t:(optimise ts)
optimise [] = []

-- Evaluator
type Tape = ([Cell], Cell, [Cell])

eval1 :: Token -> Tape -> IO Tape
eval1 In s@(ls, _, rs) =
  getChar >>= \c ->
    if c == '\r' then
      eval1 In s
    else
      return (ls, fromEnum c, rs)
eval1 Out s@(_, c, _) = (putChar (toEnum c) >> return s)
eval1 t@(Loop ts) s@(_, c, _) =
  if c == 0 then
    return s
  else
    (eval' s ts) >>= (eval1 t)
eval1 Leftward (l:ls, c, rs) = return (ls, l, c:rs)
eval1 Rightward (ls, c, r:rs) = return (c:ls, r, rs)
eval1 (Plus n) (ls, c, rs) = return (ls, (c + n) `mod` 256, rs)
eval' :: Tape -> [Token] -> IO Tape
eval' e = foldl (\s t -> s >>= eval1 t) (return e)
eval :: [Token] -> IO ()
eval ts = eval' (repeat 0, 0, repeat 0) ts >> return ()

-- Glue
main :: IO ()
main = getArgs
   >>= (\ss -> if null ss then getContents else readFile (head ss))
   >>= eval . optimise . parse

I use PowerDNS (pdns) for running DNS servers. For the primary nameserver running on a machine big enough to run a MySQL server, I use the MySQL backend for pdns. For backup nameservers, I like to be able to use a much less powerful machine, which means not running a fully-fledged SQL server. The obvious solution is to use the SQLite backend (gsqlite3) for pdns. These backup nameservers are generally set as superslaves, meaning that they'll accept any domains handed to them by the primary nameserver, rather than only accepting records from the primary nameserver for domains which it is explicitly set as a slave for (so upon registering a new domain, only the primary nameserver has to be told about it).

In a perfect world, everything would work. Unfortunately, in my experience, pdns with the gsqlite3 backend doesn't like being a superslave. If you try it, then upon being handed a new domain by the supermaster, the superslave gives the following error:

Backend error: Database error trying to insert new slave 'example.com':
Error while retrieving SQLite query results

Mailing lists suggest that this is due to a bug in the gsqlite3 backend, and that a solution is to use the opendbx backend for pdns, and have opendbx use its sqlite3 backend. This is exactly what I end up doing, so you go through the process of downloading and building OpenDBX, then recompiling pdns with support for the opendbx backend rather than the gsqlite3 backend, and rewriting the pdns configuration file to point it at the SQLite database through OpenDBX. Supposing you do all this correctly, pdns will launch, then complain about a missing d.auto_serial column, then exit, which is when you remember that the opendbx backend wants your tables to be set up slightly differently to what the pdns documentation tells you, so you remake your SQLite database using the commands listed on the OpenDBX site. Now pdns launches successfully and stays running, but upon trying to transfer in a domain, the following error occurs:

[OpendbxBackend] Database connection (write) to '/var/pdns/' succeeded 
Can't determine backend for domain 'example.com'

At this point, you're nearly ready to give up, but you decide to try one last thing inspired by the message just before the error: the user which pdns is set to run as has read / write permissions to the SQLite database file, but doesn't have many permissions on the directory containing the SQLite database file (which perhaps it needs to create copies of the database file for transaction support, who knows). Upon making the pdns user the owner of the directory containing the SQLite database, things finally work:

AXFR started for 'example.com', transaction started
AXFR done for 'example.com', zone committed

That is today's tale of woe. May it assist me in the future when I next commission another backup nameserver.

One of my courses this term is titled Concurrency, which doesn't cover programming with multiple threads and synchronisation primitives, but instead covers a language called CSP, which isn't a programming language in the traditional sense, and is more of a language for modelling and verifying concurrent systems. This post is a brain-dump of my current understanding of machine readable CSP (called CSP/M), which is aimed at nobody in-particular.

Events

We shall be considering automata, and as such we first need a (possibly infinite) alphabet. The letters of this alphabet are called events, and a family of related events is given the term channel. In any given CSP/M script, the alphabet is defined by channel declarations. The simplest form of this declaration defines a finite number of events:

channel some_event, some_other_event, a_third_thing

In this simple form, the word channel is slightly misleading, as each family of events has just one event in it. The more complex form of the channel declaration defines a family of related events name.x where x runs over a set X:

channel name : X

Finally, you can conveniently define a family of related events where the set is a Cartesian product of other sets, so the following defines a family of events complex_name.x.y.z where x varies over X, y over Y and z over Z:

channel complex_name : X.Y.Z

Processes

We shall consider a process to be a (very-)non-deterministic non-finite automaton, where every state is an accepting one, and each transition is labelled with an event (or with epsilon or tau, which we'll get to) - the literature would call this a labelled transition system (LTS). The language accepted by this automaton is given the new term of the set of traces of the process, and two processes are called traces equivalent if they accept the same language. The whole of CSP can then be regarded as a language for defining these fancy automata. To build these automata, it is useful to have a few basic processes to start from, and while the literature presents quite a few, the only ones present in CSP/M are STOP and SKIP. For now, we shall ignore SKIP, and just consider STOP. The STOP process is the simplest possible automaton: it has a start state, but no outgoing edges whatsoever. The language accepted by STOP is the set containing the empty word, so we say that the set of traces of STOP is the set containing the empty trace. A state with no outgoing edges is called a deadlock state, and so the STOP process is always deadlocked.

Prefixing

One way of building up processes is called prefixing. In the most simple form, this creates a new automaton from an old one, with a new start state which is linked to the old start state by a single transition. In the following example, a process called press_me_once is defined, whose set of traces is the empty trace and the trace consisting of just the pressed event:

channel pressed
press_me_once = pressed -> STOP

A process can be parametrised by one or more variables, where each variable can be a simple scalar value, or more complex values like sets or sequences. Combined with defining processes in a recursive way, this allows for slightly more interesting processes. In the following example, the set of traces of the process press_me_n_times(n) are the empty trace and the traces made up of at most n pressed events:

channel pressed
press_me_n_times(0) = STOP
press_me_n_times(n) = pressed -> press_me_n_times(n - 1)

With parametrised processes and families of events, there emerge more complex forms of prefixing. The first of these allows for event to be specified from a family of events based on a parameter (or any other, possibly constant, expression). The following example uses the family!expression syntax to define five processes, where the set of traces of press_me_once(x) is the set containing the empty trace and the trace consisting of a single pressed.x event:

X = {1, 2, 3, 4, 5}
channel pressed : X
press_me_once(x) = pressed!x -> STOP

The second extended form of prefixing is different to prior forms in that it prefixes a set of automata into a single automaton rather than a prefixing a single automaton into a single automaton. The following example extends the previous one with the family?new_identifier syntax, so that the choice process prefixes all of the press_me_once(x) processes, with the set of traces of the choice process being the set containing the empty trace, the traces choose.x for any x in X, and the traces choose.x pressed.x for any x in X:

X = {1, 2, 3, 4, 5}
channel choose : X
channel pressed : X
press_me_once(x) = pressed!x -> STOP
choice = choose?x -> press_me_once(x)

This syntax can be extended to family?new_identifier:subset to restrict the prefixing to a subset of the family of events rather than the entire family. From this, we see that family!expression and family?dummy:{expression} have the same meaning, apart from the latter introducing a new dummy variable. For families of events constructed from the Cartesian product of multiple sets, this syntax extends to allow multiple "!" and "?" clauses, though these clauses should not be inter-mixed with "." clauses from simple prefixing (use a "!" clause with a constant expression where you want ".").

Internal and external choice

Prefixing is one way of constructing new processes from old ones, which involves added transitions labelled with events. On the other hand, choices construct new processes from old ones using epsilon (external) and tau (internal) transitions. External choice is the simpler of the two types of choice, and is similar to the union construction on NFAs. In its most basic form, the external choice operator (denoted []) takes two processes and constructs a new process whose initial transition is any of the initial transitions of the two original processes, and then proceeds like the chosen original process. For example, the traces of the following bebop process are the empty trace, and the singleton traces be and bop:

channel be, bop
bebop = (be -> STOP) [] (bop -> STOP)

This operator generalises to external choice between a set of processes rather than just two processes by the syntax []identifer:set@process(identifier) meaning that the following example defines the canonical RUN(X) process, which given a set of events X (not necessarily from the same family, hence precluding use of prefixing with a "?" clause), has a set of traces where each trace is made up of a finite non-negative number of (possibly repeated) members of X:

RUN(X) = [] x:X @ x -> RUN(X)

Internal choice is much more subtle than external choice, and the trace set concept is not sufficient for appreciating its semantics. Given two processes P and Q, the internal choice of P and Q is denoted P|~|Q, which is a process which behaves like P or like Q, but with the choice between the two taken immediately rather than delaying the choice until a subsequent properly-labelled transition is taken. The following bebop2 process is either an NFA which accepts the empty word and the word be, or an NFA which accepts the empty word and the word bop, but you do not know which until you actually simulate the NFA:

channel be, bop
bebop2 = (be -> STOP) |~| (bop -> STOP)

The set of traces of bebop2 is the same as the set of traces of bebop, as any given trace of bebop can be a trace of bebop2, just that sometimes it won't be. Like for external choice, there is a generalised internal choice operator which chooses between a set of processes rather than two processes, the syntax for this being |~|identifier:set@process(identifier).

Parallel processes

All the previous ways of combining processes are fairly sequential, and involve one process "running" at a time. The parallel operator spices things up a bit by allowing multiple processes to be combined into a single process which represents all of the original processes running in parallel, similar to the product construction on NFAs to allow one the simulation of multiple NFAs to be done by the simulation of their a single NFA representing their product. Given two processes P and Q, and a set of events ES, the syntax P[|ES|]Q denotes the parallel execution of P and Q, with the restriction that for every event E in ES, transitions labelled with E can only occur when P and Q perform them simultaneously. Like other process-combining operators, there is the generalised form [|ES|]identifier:set@process(identifier) which represents the parallel execution of all the involved processes, with the restriction that events in ES must occur in every process simultaneously.