Design of the Kernel Language for the Parallel Inference Machine

Looks like all my fooling around with cobs and application-level scheduling is very similar to Flat GHC/KL1 from the Japanese Fifth Generation Computer Systems project.
They were doing this stuff when I was learning my first programming lessons :)

PS: actually, http://citeseer.ist.psu.edu/ueda94moded.html is closer to my ideas.

Simultaneousity induced by causality

A really quick note - when lifting functions to event processing, their inputs must happen simultaneously. One idea for simultaneosity in absence of global clocks is to define events as simultaneous iff their causes are equal.

More generally, all uses of timestamps might be replaced by causes. All these partial orders start looking similar to domain theory...

I will need to check how far this can get me.

Unitstreams

Another random thought:

I got curious, what would be the minimum abstraction needed to describe communication between agents. One obvious solution would be bitstreams (streams of booleans). On the other hand, it is not the minimal one - if one thinks about computer networks, at the electrical level they do not use streams of bits. Superficially, setting potential on the line to either low or high can be thought as sending a bit, but actually the bitstreams sent this way are very limited - namely only streams with alternating bits can be encoded this way. And informational difference between all streams of units and those streams of bits where bits alternate is very small - just one bit per whole stream! By that I mean that a timestamped sequence of units [(), (), ()] corresponds to one of the two timestamped sequences of bits: either [0, 1, 0] or [1, 0, 1]. This difference is so negligeble, I believe it can be ignored, so we can pretend that computers communicate to each other using unitstreams (at least at some level). It is very crucial that units in these streams are timestamped, otherwise they cannot carry enough information. Networks rely on the fact that peers are usually not moving fast enough relatively to each other, so their local clocks are good enough to recover timestamps that are not sent explicitly. An interesting question would be whether it is beneficial to model clocks as unitstreams as well, then instead of timestamping units in the stream we instead relate them to units in some other stream (but probably need to ground this induction somewhere - or make it coinduction :) ).

Causality

Denotational semantics of processes is often though of as functions from input stream to output stream.
I already argued that streams are not general enough to represent communication between processes, but let's keep the model simple.

Function from stream to stream fails to represent one crucial property of the process - which input message must have been fed to the process in order to observe a specific output message. I do not mean data dependency here, but something like control dependency, or causality. Streams (or full orders) are a special case of partial orders that can be used to model causality, so there seems everything is ok - except there is no ordering between elements of input stream and output stream.
Imagine a function from stream of unit to stream of unit:

data Stream a = Message a (Stream a)
type X = (Stream ()) -> (Stream ())

There is just one function of type X - identity (non-termination is out of equation as we are talking math functions, not Haskell functions).
On the other hand, there are multiple different behaviors that accept empty messages and output empty messages.
One would be an identity behavior - for each input message send one output message. Another would be a counter - for nth input message send n output messages. By applying a function from Nat to Nat to the definition of the counter, one obtains a new behavior: for nth input message send f(n) output messages. Thus there are infinitely many observably different behaviors of this type, and trying to denote them by a single function is unsatisfactory at least.

So, the quick solution seems to define a process as a function from input list (a prefix of stream) to a list of outputs produced after receiving the last input (so the whole output list is obtained by concatenating output lists for all prefixes of the input). This may work for a single input stream, but for multiple streams we need to encode which stream received the last message.

A more general way to look onto this is to say that a process extends a partially ordered set of input messages to a partially ordered set of both input and output messages, with a constraint that it does not introduce PO links to an input message (but obviously is allowed to introduce such links from an input to an output, or between two outputs).
Need to think of a formal (and elegant) way for saying this.

Agents as frontiers of futures (or arachnoagents)

Imagine truly concurrent constraint programming, but without entailment, or any other appeal to logic. In fact, let's try to separate causality from mechanism of specification of interaction.

It may be easier to approach this task from FSM angle, or more precisely, ISM - interacting state machines.
Unlike ISM, our machines (cobs?) do not communicate via FIFO streams of messages - to model causality fairfully, a more rich structure is needed (a cobweb).
Each machine can be thought as crowling along links of immutable network of message nodes, producing another network as its output (to be traversed by other machines). Traversion is not destructive - network nodes not referenced by any machine operatonally are GCed, while denotationally they have infinite lifetime.
FIFO streams are a special case of network with strictly linear links.
To support growth, immutable networks have future nodes (promises) at their frontier - and exactly these nodes are referred (and fulfilled) by the owner machine (hind legs of the cob). Readers of the network cannot get past these growth points (with their front legs) until creator resolves them - a typical future/promise, but probably with more low-level operations than usual.
A machine is a unit of authority, while execution as such can have finer grained units.

Marshalling as a game

Investigate the problem of what to put on wire when marshalling (serializing) objects.
Some runtime environments force this decision, at least when it comes to data/code dichotomy.
When it comes to code-is-data view, it becomes very unclear, what should be transferred - think of the reflexive tower - should it be unraveled to its (infinite) roots, or at least down to the fixpoint? What if the receiver of the stream already shares some part of the tower with the sender?
In general, how can they engage in a negotiation that minimizes not only the size of the stream, but also the size of negotiation itself?

It looks it is not really about streams (that's why I do not really like the term serialization), but about identifying the part of the object that needs to be copied, and then grafting that part onto the receiver's view of world).

"It's machines all the way down" language

Seeing how concurrency support steadily becomes a must-have for a programming language, it's very sad to observe that details of scheduling concurrent processes are almost always hidden from the programmer.

{Rant about resource-aware programs}.

Would not it be good to allow the programmer to explicitly provide schedulers when needed? And resource management in general.

The idea of what I am thinking about goes as follows:

Execution history of the program forms a tree, where root represents start of the execution (initiated "supernaturally"), edges represent causality, branching represents concurrent execution, some leaves are final and represent completed (quescent??) execution, while other leaves are "growing points" and represent schedulable resumptions or input requests (there is actually not much difference between these later two, you can think about them as tokens in Petri nets). The tree is unfolded by executing resumptions by (potentially) multiple evaluators (machines?), guided by program-provided schedulers (constraints?). Each resumption is a function from evaluator's input to a tree (which can be a final leaf, an input request or a new resumption (growing point leaves), or a more complicated structure). Whenever an evaluator chooses to execute a resumption, it runs it on an input determined by the resumption's position in the tree, and then grafts the resulting tree under the resumption (probably recording the input as well, which may be useful when input is not _uniquely_ determined by the path).

Virtual machines
To make execution concurrent, resumption may return a "VM" node containing a virtual machine - with its own execution tree and a scheduler. The key is to be able to define the scheduler in the same way as "user" programs.

Another option is to return a "conc" node containing multiple resumptions - these will merge into the pool (err, tree) of resumptions controlled by the current (virtual) machine, and, respectively, scheduled using its scheduler.

Schedulers control only fairness of resource consumption, while all synchronisation issues must be dealt with by using "promise".

Issue: in this design, program is able to consume only one resource at a time - namely, the machine that executes it. How to model multiple resources? And why?
Also: explore potential for join of multiple resumptions - it's dual to the previous - one resource is simultaneously (and even atomically) consumed by multiple processes.
Also: where trust/ownership/responsibility comes into picture?

Also: vau?

Membrane contest

I am sure there will be enough people knowing the languages mentioned by Paul, and willing to participate.
I wonder, whether I'd better follow a different way, and design a language specifically for implementing membranes... But that would be E.

Another idea is to explore membrane as a game. 3-player game. A good reason to criticise theories that emphasise 2-player games?

Socially Responsive, Environmentally Friendly Logic

This logic looks very interesting, as it covers multiple players.
I still have to understand whether it also supports true concurrency in the sense used in CCP.

Away for a week

I am away for a week to a sea-side, may spend some of this time thinking about Goedel's incompleteness theorem.

A Hyperdoctrinal View of Constraint Systems

The title sounds scary, but this paper is quite thoughtful and looks crucial to understand the importance and beauty of concurrent constraint programming.

Intuitively, CCP is good because it is so easy and natural to define a denotational semantics for it. This naturality stems from the fact that closure operators are completely defined by sets of their fixpoints, so all combinators on them can be defined in terms of this sets, not functions themselves. And ability to limit attention to closure operators follows from informational approach to computation.

Internal Type Theory

In a previous paper I introduced a general notion of simultaneous inductive-recursive definition in intuitionistic type theory. This notion subsumes various reflection principles and seems to pave the way for a natural development of what could be called ``internal type theory'', that is, the construction of models of (fragments of) type theory in type theory, and more generally, the formalization of the metatheory of type theory in type theory.
The present paper is a first investigation of such an internal type theory.

I am currently reading this paper (when not working on my day job), so the interpreter has to wait.

Open scheduler. Or open language?

I just wanted to add yet another feature to PAL - fairness for units bigger than a single continuation.
Round-robin for continuations is simple, but it does not take into account the creators of continuations (cause/effect tree). As always, it is possible to construct a use case where right scheduling means not only difference in performance, but also in termination; but I will not do that.
Basically, PAL needs a construct to give a programmer control over dividing "CPU time" between sets of continuations. This could be done, for example, by a statement (SplitCPU PerCent Statement Statement) that reduces two statements in parallel by allocating PerCent "CPU cycles" to the first one, and 100-PerCent to the second one. These statements compose with other statements and each other in an obvious way (children sharing percantage of their parent, not the whole 100%).
This looks cool, but what if I want to introduce more constructs? Already I need cancellation of a branch and scheduling of non-CPU resources ("oracles", more on this later). And I see no easy way to implement these constructs via compilation to PAL.
At this moment I decided - why not make PAL user-extendable? It already supports user-extended terms, I plan to support user-provided scheduler, then why not user-provided statements (op-codes)?
In fact, the whole PAL can be just a composition of a set of "features", where each feature is a set of statements, terms, and scheduling rules. The current PAL can be split into three features - promises, cells, and atomic execution.
I already compose terms using a fixpoint of multiple term functors (actually I mix one functor into a base term, but maybe there ways to do that for any number of functors), I hope the same can be done for statements, but composition of schedulers (reduction strategies) looks a bit less clear at the moment.
If this indeed works, I believe it's time to either create a SourceForge project, or write a paper, or both :)

PS: I have to remember to document my thoughts on efficient implementation of the execution trace tree in the light of composable features.

Plain interpreter. No, compiler.

I was a bit ill during the weekend, so instead of going to seashore played with Haskell.
I shot for an interpreter of Plain in Haskell, but ended with a compiler from Plain to a STM-like intermediate language (promises and atomic execution - let's call it PAL) and an interpreter for PAL in Haskell (let's call it PVM). This looks promising (pun intended).

What I need to do before going further is:

1. Fix implementation of variables in PVM (this is currently a strange hybrid of de Bruijn indices and dynamic scoping).
   
2. Express PAL statements in monadic form to simplify writing compiler(s).
   
3. Express PVM in monadic form to simplify experimenting with it.
   
4. Externalize scheduling (probably in a way of A Language-Based Approach to Unifying Events and Threads). Amusingly, an atomic execution could be elegantly expressed as a strict node in the trace tree.
   
5. Explore possibilities for a type system for PAL (A Functional Abstraction of Typed Contexts?).
   

Typed Concurrent Programming with Logic Variables

We present a concurrent higher-order programming language called Plain and a
concomitant static type system. Plain is based on logic variables and computes
with possibly partial data structures. The data structures of Plain are procedures, cells, and records. Plain's type system features record-based subtyping, bounded existential polymorphism, and access modalities distinguishing between reading and writing.

You may want to compare this with The Oz Programming Model (OPM), which

... is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming.

Another paper on OPM is The Operational Semantics of Oz.

In short, the model of Plain is based on that of Oz with the main differences being:

1. Plain statically types programs using a type system with subtyping, while Oz is latently typed.
   
2. Therefore Plain chooses to drop support for unification in favor of a single-assignment operation.
   

Logical variables?

After all, it looks like old good logical variables may be the best solution for a communication between objects.
See, for example, An introduction to AKL (a precursor of Oz).

Typed Logical Variables in Haskell looks like a good introduction to typed logical variables in Haskell (hey, that's written in the title :) ).

Backtracking

Well, STM's retry is so to say pessimistic - it restarts the whole transaction (up to "atomically" or "orElse") instead of backtracking a single step (one "bind").

Using (simple) backtracking can be inefficient. As an example, consider again a binary join, which succeeds if both its inputs succeed:

join [([], []), ([1], []), ([1], [2]), ([1, 3], [2, 4])] = [([1],[2]),([1],[2]),([1],[4]),([3],[2]),([3],[4])]

It can be implemented for any MonadPlus, but there is some inefficiency there:

join :: MonadPlus m => m (m a, m b) -> m (m a, m b)
join sab = do
  (sa, sb) <- sab
  a <- sa
  b <- sb -- failure on this unneccesary retries sa, should retry sab
  return (return a, return b)

What's worse, there is also a difference in semantics. Consider a shocking example, which fails to terminate:

join [(repeat 1, []), (repeat 1, [2])] = ⊥

This would produce a single answer, and THEN fail to terminate, if it retried sab after failing to read sb:

join [(repeat 1, []), (repeat 1, [2])] = [(1, 2), ⊥]

Note that I cannot fix join by simple moving b <- sb before a <- sa, as they are fully symmetric. What I need is a combinator, which unlike bind would execute actions in parallel, and fail AS SOON as any of them fails. Let's say I need a parallel and - pand. Can I code it in terms of MonadPlus? Let us see...
Aha, a quick googling got me A Monadic Semantics for Core Curry.

Software transactional memory = optimistic transaction isolation + backtracking?

While playing with STM, it occurred to me that it actually combines two features: optimistic transaction isolation (OTI), which allows transactions to execute seemingly independently of each other, and backtracking (BT, implemented via retry/orElse/bind in place of fail/or/and), which ensures atomicity.
If one takes care when designing a concurrent language, then OTI becomes unnecessary. For that, it is sufficient to have:
NDW: non-destructive writes - the source of communication cannot undo previous actions, it can only "append" to them.
LRD: localised read and destroy - access to read/destroy operations on communication media is tightly controlled and in some sense local (like a single thread).
MB: monotonic behaviors - behavior cannot fail on an input bigger than one which made it succeed.
Join calculus enjoys all these properties. Indeed, NDW is ensured by writes appending to a multiset of messages, LRD is ensured syntactically by coupling creation of channels with specifying reactions to them, and MB is trivial as well - join calculus behaviors can only fail (which means - block) because of lack of a message, not because of an extra message.

Why do I think that NDW+LRD+MB obviate OTI?
Because MB ensures it's ok to schedule producer a bit sooner, BT ensures it is ok to schedule consumer a bit sooner, and NDW+LRD+MB ensure it is ok to run producer and consumer in parallel.
One still has to be careful at a very low level of operations - e.g., the multi-processor implementation must ensure atomicity of single writes and reads, but this is easier then full OTI.

If I am right with this conjecture, it would be cool to try and split STM into two facets, OTI and BT, and see, what happens.

BTW, isn't BT just a fancy name for Control.Monad.List? :)

Maude

I am away reading Maude 2.0 Primer.

A Language-Based Approach to Unifying Events and Threads

Looks like great minds think alike :-)
I have to read this paper to see if I am reinventing a wheel.

Some examples from E

I had ten minutes before lunch, and decided to code up a couple of examples from E in Haskell:

type Cont a = a -> STM ()

-- Blocking caretaker - requests are blocked until the gate is open
-- Note that the gate can be opened/closed repeatedly.
makeCaretaker :: Cont a -> STM (Cont a, Cont Bool)
makeCaretaker target = do 
  enabled <- newTVar True
  return (\m -> do {e <- readTVar enabled ; if e then target m else retry}, writeTVar enabled)
  
-- Overwritable promise.
makePromise :: STM (Cont a, Cont (Cont a))
makePromise = do
  queue <- newTChan
  target <- newTVar Nothing
  return (\m -> do
    t <- readTVar target
    case t of
      Nothing -> writeTChan queue m
      Just r -> r m
    , writeTVar target . Just)

Note that both caretaker and promise allow the controller to change its mind - either by repeatedly opening/closing the gate, or by re-resolving the reference. Also, when closed, the caretaker does not signal errors or swallow messages - it keeps the senders blocked. OTOH, promise stores messages in a queue.
Of course, this can be changed (I leave this as an exercise for readers :-) ).
I may consider creating a small library of such patterns and see whether something DSLish comes of it...
But before that I must decide on verification procedure - should I use unit tests or proofs...

STM for CPS

I am trying to manually code up some simple programs using a -> STM () as a continuation type...
And, well, I've stumbled upon some problem with types. Consider a type for a cons list expressed in CPS:

type List a = ((STM (), (a, List a) -> STM ()) -> STM ())

The first STM () gets executed in case of Nil, the second in case of Cons (getting a pair of car and cdr).

Unfortunately, this type fails to check in Haskell. I have to grok yet why, and how to work around it. I would hate to use data:

data List a = List ((STM (), (a, List a) -> STM ()) -> STM ())

as this would reduce clarity by boxing unboxing. Compare:

makeNil :: List a
makeNil (caseNil, _) = caseNil

and

makeNil :: List a
makeNil = List $ \(caseNil, _)->caseNil

Then again, if I shoot for terseness, then nothing beats:

makeNil :: List a
makeNil = List fst

Envisioning code generation for algebraic data types, I arrive to:

type Cont a = a -> STM ()

type CaseNil = Cont ()
type CaseCons a = Cont (a, List a)
data List a = List {unList :: Cont (CaseNil, CaseCons a)}

makeNil :: () -> List a
makeNil payLoad = List  $ \(caseNil, _) -> caseNil payLoad

makeCons :: (a, List a) -> List a
makeCons payLoad = List $ \(_, caseCons) -> caseCons payLoad

Hmm, I should consider using currying, after all...

Critique

The ideas presented so far are not even close to supporting join calculus (however simple it is).
Fluid still falls short in several areas: it is (practically) first-order (so messages do not carry references), it does not support creaition of objects at runtime, it is data flow driven (call it pull-only, or lazy, if you please).
The first problem is caused by the third, which is caused by input devices being the only active sources of messages.
This was caused by the decision to represent outputs of instances as transactionally lazy (STM a)'s, which promised better composability.
Basically, the choice (for a very simple case with one input and one output) is between:
STM i -> STM o -- transaction transformer paradigm, precludes "push", as only the receiving side of the reference is active
and
STM i -> (o -> STM ()) -> STM () -- hey, looks like monadic bind!

BTW, I suspect that relationship between these two types can be seen as expression of some property of negation in some logic :-)

Devices/distribution = chicken/egg?

Obviously, I/O devices and distribution (multiple vats) can be expressed using each other.
For various reasons I prefer to view devices as primitive, and implement distribution via stubs/scions (this is consistent with E paradigm).

What is not consistent with E paradigm, though, is that a vat ceases to be a single thread - it is a family of threads, namely one thread for (transactional) instances, and one thread for each device. I cannot understand the implications at the moment (mostly for robustness), but this is something to keep an eye on. OTOH, I can always bind this family to a single OS thread, which means I will match E perfectly, right? Must ensure this way of running vats is enforced, though.

Some code functions+devices

Here is some Haskell code to illustrate my previous post (I cheat a bit with tuples in unary cases):

-- AND join in workflow terminology.
binaryJoin :: (STM a, STM b) -> STM (a, b)
binaryJoin (sa, sb) = do
  a <- sa
  b <- sb
  return (a, b)

-- Very simple code function.
inc :: Num a => STM a -> STM a
inc sa = do
  a <- sa
  return (a+1)

-- Code that delegates to other code.
add :: Num a => (STM a, STM a) -> STM a
add inputs = do
  (a, b) <- binaryJoin inputs
  return (a+b)

This code covers so called instances in terminology of Mark's thesis.
What about devices? For output the answer looks simple: code for output devices has type:
(STM i1, ..., STM im) -> IO (), but such object would probably require a separate thread to run (can we say that's because, unlike STM, IO is not composable?). Thus, I suggest splitting (code for) output devices into a transactional matcher part (if needed at all) of type (STM i1, ..., STM im) -> STM a and a reactive handler part of type a -> IO (). This gives the framework runtime a chance to run matchers transactionally, and only when one of them matches, run the handler.
So, we have (pseudo-Haskell):
data OutputDevice = forall a . OutputDevice ((STM i1, ..., STM im) -> STM a) (a -> IO ())

What about input devices? The first idea is to type them:
(a -> STM ()) -> IO ()
with the contract that the device performs some input, then applies the (parameterised) transaction to it, then runs it.
Why not just IO a? Deal, I can minimize input device's responsibility by saying the framework will "apply and run", while the device will just read and return, so the type is:
IO a

Well, by its nature (blocking input) each input device will be run on a separate thread, injecting its values into the transactional thread via TChan'nels. I don't like this (especially when we dealt with multithreading issues of output devices), but currently see no other alternative. I have to explore the Haskell standard library to see, whether the input is mostly blocking.
If nothing better can be done with input devices, then maybe it makes sense to run output device on separate threads as well, and let STM runtime to handle blocking (so output devices will be typed (STM i1, ..., STM im) -> IO (), or even a -> IO ())...

Some thoughts

Ok, I decided to stop fighting Haskell on the particular technical issues, and instead sit back and think a little.

What is an object? From the implementors point of view, of course :-)
Let's assume in E tradition that this is something that upon receiving a message can change its state and post a set of messages along the references it holds.

Nothing interesting so far. It becomes better when we notice that multiple objects often share some logic, which we might call "code" or "class" or "prototype". Let's call it code. What is this code? In Haskell, I postulate, it is natural to see this code as a function from message and object state to set of deliveries and new state. But what is the exact type of this function? Here some experience with join calculus suggest a nice trick: both the state and the messages can be modeled uniformly!
My current proposal is to say that object code is a function of type:
(STM i1, ..., STM im) -> (STM o1, ..., STM on)
The inputs are transactions that represent reading either public "facets" or private "state", and the outputs are transactions that represent either sending messages to other objects or updating private state (in a roundabout way - the transaction must be executed to obtain the "written" value - this simplifies composability of multiple code functions).
(Of course this type can be curried, but I like its simmetry).
is and os stand for (possibly polymorphic) types (not sure yet how to better handle multiple messages on the same ouput - and then, maybe on the same input, as well?).
Note that none of the output types mention the identity of the receiver - they are indeed types of messages, not of deliveries.

So how and who attaches the receivers to the messages? I say it is responsibility of (the instance of) the object that uses this "code". Note that I ended up with three parties: authors of the code, users of the code, and authors of the framework (that's me!) that are responsible for helping users to use the code easier. Now if only this third party knew how to achieve that :-)

No Data.Typeable for polymorphic types :(

Alas, after spending some time with Data.Typeable I understood it is (for some reason) limited to monomorphic types.
Thus I hesitate to use it as a way to glue (user) delivery handling functions to the (system) framework.
Hmm, should I invert the logic, and instead of functions from (reading) STMs to Effect use tuples of (writing) STMs and Effect?

Probably I will get smarter after lunch :)

The first problem

Well, I have the first subset of runtime working - objects with a single facet (so state or concurrency are not possible).
That was surprisingly easy, despite I needed to understand existential types.

Now I have the first problem - to introduce multi-faceted lexical compounds I need to write a function taking a function from several (let's say n) STM Delivery to Effect and returning exactly n TChan Delivery and an Effect...
A wrong type:
close :: ([STM Delivery] -> Effect) -> ([TChan Delivery], Effect)
as it does not constrain the lengths of the lists to be equal (and worse, operationally close does not know how many channels to create given just a function from a list to effect).

When I figure out how to do this (either by adding explicit n to the left side of the type, or by some GADT trick), I will generalize the problem to parametric (Delivery o a)...

Kick-off

Ok, I said I will "try and create a toy implementation of E-like system", and so I started this blog to document my thinking and its changes.

First of all, I am happy to start working on this, as my previous experience with Haskell was limited to school assignments - now I can finally use all the cool features, including type classes, existential types, composable transactions, and more :-)

I quickly rolled a parser for join calculus using Parsec, not that this was needed at the moment, but it was fun and a good warm-up.

Now I am pondering over the ways to skin... err, to modularize the runtime.
One idea is to have multiple languages interoperating in my vats (word "vat" is used without permission of E authors :-) ), so I want to separate semantics of the process definition language from that of the "robustness framework".

I will start from defining the notions of delivery (or message), object (the target of deliveries), and effect - what happens upon delivery. I need at least IO effects to model output devices (in terms of E thesis), and also (STM [Delivery]) effects to allow objects send messages to other objects (transactionally - in the same vat). I think I will need forall to allow multiple implementations of objects to cooperate... Time to learn some Haskell-fu :-)

BTW, if you wonder: Fluid is the code name of this project.