Lambda the Ultimate

I really don't get this. How do you stop an actor being shared. When I compile a code module I have no idea which threads are going to call my actor.

It seems actors break separate compilation, which makes them unusable for any general programming language where compiling large programs is a must.

Lexical scope.

If I have a maths library of common maths functions like factorial, how would I get local, lexically scoped copies of these actors?

If the actors are pure, I don't think we actually need local lexically scoped copies, as they have no state.

We only need local copies of stateful actors. How can I tell the if an actor is stateful to determine if I need a local lexically scoped copy?

But even with lexically scoped actors, it does not seem trivial to determine if multiple threads can simultaneously call the actor.

Edit: To clarify, it seems we need a type system that tracks effects, or has monads like Haskell, so that whether an actor is pure or impure can be tracked in the type system. A pure actor can be used direct from the definition without instantiation. An impure actor needs to be initialised (in a lexical scope thus controlling sharing to some degree). I am still not clear how decisions to parallelise (requiring mutex locks) or serialise actors would be taken.

It's up to recipient how it processes a message. If the recipient claims to be cacheable (i.e. same response for same message) then the infrastructure can cache responses.

Of course, no matter what the implementation mechanism, a shared financial account must deal with contention in massively concurrent systems.

Caching responses is going to be slower than just running the actor for small actors. Especially as the cache will need mutex locks for updating the cache when used from multiple threads. The pure version can be shared between threads without needing any locks.

It seems to me we need to be able to determine if an actor is determinate in the type system (Monads do this), we need to be able to track side effects (So an effects system is needed in the type system too). We also need to be able to represent thread access in the type system so that we can implement:

,---------,---------------,--------------,
|         | single thread | multi thread |
|---------+---------------+--------------|
|pure     |   no mutex    |   no mutex   |
|---------+---------------+--------------|
|stateful |   no mutex    |    mutex     |
'---------'---------------'--------------'

If we can track the information in the above table in the type system we should be able to keep the use of mutexes to where there really are multiple threads accessing a stateful actor.

that it's worth it to invest the time.

For instance on a simple symmetric multiprocessing system, I'd do my usual vm tricks:
1) one system thread per core or per hardware hyperthread, green threading within each system thread
a) this allows nearly free locks within each system thread (but not touching the other threads)
b) this allows synchronization between ALL threads at a cost only commensurate with the number of hardware cores, since context switches only happen at safe points
c) this sort of system is almost necessary for high quality, parallel garbage collection anyway, and is used (I think) by both java and .net

2)actors that aren't pure (and therefore need to be synchronized) are owned by a given core/system thread
a) they only need one set of i/o queues per core
b) since writes to a given queue are always by the same core, no synchronization primitives are needed on processors like Intel. On processors like current generation Arm, then there will need to be some cache flushing per message that communicates with a different core. Arm is a worst case where there needs to be a synchronization instruction on load if there is even a possibility that something was written by a different core so the best you could do on Arm is to aggregate a bunch of unrelated message checks with one synchonization instruction.
c) I originally forgot to add: a call on an actor from the processor that owns it is just a function call. And on a processor like Intel a check for which thread owns it can be unsynchronized. If you want a check like that to be unsynchronized on Arm, then you'd need to sync all of the processors whenever an actor switched owning processors.

Note: Arm 8 promises to be the first implementation of C++ memory model in hardware. At this rate it will never be released, so by Arm I mean 7 or under.

I am reasonably sure an effect system modelled by parametric monads and row polymorphism can track the purity and impurity of actors in a way that does not limit parallelism.

The interesting question for me is how to track the number of threads that may send a message to an actor. The number of threads is something like the number of messages in flight at a time. If all the actors wait for a response after sending a single message, and we start the program by injecting a single message, then there would only ever be a single thread needed. If an actor sends messages in parallel to the same recipient they have to be sequentialised. So the only time we introduce new threads is when an actor sends multiple messages in parallel to different receivers, and the only time we need a lock is when these different receivers, or actors they message, message the same actor.

As we have to know the "address" of an actor to message it, the above condition becomes, an actor needs a mutex if its address is sent to more than one actor in parallel, which each then use the address.

It should be possible to capture this information in the type system using monadic effects. If there is an effect for sending a message to address X, then this tracks sequential messaging within a thread. The tricky part is we need the effects to combine differently when messaging multiple actors in parallel that may message the same actor.

I don't even know what that stuff you wrote meant, but at the bottom, processors (some of them) have read and/or write queues on memory - these are hardware level, not instruction level.

If multiple processors are going to communicate, they have to have a design that works with those queues, and those designs can either be naive ones with lots of slow instructions that make those queues flush and wait for them, OR they can be designed as I posted to finesse the actual behavior of those queues and match it to needs. The design I mentioned trades memory for locks and limits the amount of memory needed to the number of processors, at a further cost of changing the threading model. But it also means that the system can optimize actor methods by making calls from SOME THREADS cheap.

I don't see how your gobbletygook changes that, underneath all your abstractions, you still need a mechanism for synchronizing memory between processors, especially on processors like Arm that make no guarantees and essentially can have NO kinds of safe memory sharing without synchronization instructions. Although it's on processors that have some guarantees where you can actually finesse the code to be most efficient. But aggregating synchronization on Arm is a big win over naive too.

I was only talking about the case of impure actors.

So I was assuming that you had already sorted the pure ones from the impure ones.

I am assuming we have already sorted pure from impure actors (using some kind of monadic effects, and tracking this in the type system). I was discussing tracking whether an impure actor is ever passed a message from more than one thread. So even if an actor is impure, if all messages sent to it come from the same thread it does not need a mutex lock.

My idea makes SOME calls a lot faster but others even slower if latency counts - though I can imagine a work around.

My design, rather than depending on mutexes, depends on queues being processed in another thread, when they're noticed, which should make message latency very high - but since it doesn't rely on synchronized instructions it could make a system with enough parallel work have better throughput.

A work around could free unused actors from their thread if they go unused for long enough - in that case calling one costs as much as a mutex, but only if they've been freed.

You wrote:
"As we have to know the 'address' of an actor to message it, the above condition becomes, an actor needs a mutex if its address is sent to more than one actor in parallel, which each then use the address."

First of all, it's work for the programmer to convince the compiler that only one thread has the address of an actor at a time. More work than it's probably worth.

Second of all, I was saying that you can optimize for calls from a group of thread WITHOUT there being limits on who can call that actor, it's just that calls from the wrong threads will wait until they're handled.

Note, that switching ownership between threads isn't cheap unless you can prove to the program that there is no possibility of messaging from multiple threads so see objection 1, that proving this to the compiler would be a lot of work.

*****

Consider the case of optimizing a system like the one I described - that would be a matter of trying to untangle the web of calls to balance the load while reducing the number of messages that have to wait.

Also if the speed of communication between threads depends on those threads sharing a processor, then scheduling is more constrained than is traditional.

Perhaps one just uses hints from the programmer. I'm a fan of run-time profiling and analysis. Or whatever you call it when you do some runs for analysis and then use the data from those runs to recompile with better optimization.

Even though an actor design is one way to attempt to make parallel algorithms reliable, it can't make communication between different processors fast so you:

1) design a program with large chunks that are expected to run on a single processor. Code is all labeled by which chunk it's in.

2) the system is free to assign these large chunks among processors or move them, but as a whole.

3) there can be connections of different strength between the chunks so that more strongly connnected chunks tend to be on a single processor, or weakly connected ones always go on separate processors for efficiency

I agree that green threads running on each core, with locks makes sense. There may also be efficiencies that can be gained from cores sharing a cache (mutexes can be in cache, rather than in main memory).

I think that makes sense if you are modelling message passing using actors written in some other language.

I was trying to imagine a way of compiling that could make actors all the way down comparable in efficiency to an imperative languages, hence why it is important to know if actors are only used sequentially.

to build something like Self or Smalltalk or some such on message passing concurrency.

Functions aren't actors in that they return values back and whatever invoked them waits for an answer... c2.com has a page on actor languages that claims that scheme came from an attempt to understand the actor model followed by a paragraph that I suspect was written by Hewitt:
Sussman and Steele arguably got continuations wrong; continuations in the actor model do not have the security problems that caused them to be omitted from DoubleYouSeven. In particular, Scheme continuations can return more than once to code that is unprepared for this. In the actor model, OTOH, an actor can be written to respond a continuation more than once, but that would have to be explicitly programmed. Also note that actor continuations are a derived concept, whereas in implementations of Scheme they have to be supported as a primitive.
( here http://c2.com/cgi/wiki?ActorLanguages )

It's not clear to me how that would work, but typing a function for continuations that capture it is interesting.

Note, I just followed the link on that page to Actor Prolog, which while that looks a very nice discussion, it's using a totally unrelated meaning for the word "actor" and so doesn't belong on that page.

Functions aren't actors in that they return values back and whatever invoked them waits for an answer.

This isn't difficult to support by binding an invocation result to a future. The E language distinguishes method 'send' from 'call', where 'send' does this binding implicitly.

If you send the resumption or continuation with the message, and then stop, then the result is the same as a function call.

I would have thought it would be good to have a function-call like syntax for this, because languages like JavaScript that have event models are awkward to program.

I hope no one is expected to use that without syntactic sugar.

Procedures are Actors with message passing, e.g., Factorial.[3]

Is that supposed to work by sending a message containing "3" and the continuation to call with the result to the "factorial-actor"?

A request conceptually have a customer Actor. A customer Actor can be sent a return or a throw communication.

Has that changed from the earlier descriptions with continuations? When a actor sends a request to a customer, does it wait for the reply/return?

Customer Actors are ancient; continuations in cheese are new.

Why did you explain using customer actors in the post before last, only to tell me later that is out of date?

So what would a function call look like using the newer model?

customer is "not out of date".

Why would you have two models for message passing when one subsumes the other? What's wrong with sending the continuation with the message? If forking a new thread is explicit, then you can capture both options, you either send a message with the continuation without forking (works like a function call) or send a message with a continuation in a new thread.

________________________________________________________________________

Conceptually, the address of a customer Actor is sent with a request.

Continuations are a concept used in ActorScript to structure execution in cheese.

So when I write an actor program like:

print[f[3]]

What determines if I wait for the reply to the message '3' sent to 'f'?

Type, address, and recipient Actor determine how a request is processed in ActorScript.

If you could send a continuation with any message, and either send the message in the current thread or in a new-thread, then you could re-use other actors more, as the same message handler could be used synchronously (like a procedure call) or asynchronously (like starting a new thread).

If the receiver determines the message semantics, then common functionality needs to be implemented twice for the synchronised (procedure call) and asynchronous (message passing) communication methods.

Threads are a terrible conceptual model of concurrency causing much confusion.

Of course, low level implementation mechanisms, e.g., registers, coherent memory, caches, stacks, threads, etc. can be very useful.

Maybe, but how else can you implement concurrency? A thread is defined by having the same memory and resources (so we don't have to reprogram the MMU all the time), but a different stack for local variables.

In terms of implementation I don't think there are any alternatives, better or otherwise.

In terms of the model, all I am suggesting is that the sender determines whether to wait for a response, rather than the receiver. This seems better for code reuse as the same actor message-hander can be used in both cases.

[Pretty much what Hewitt already said in reply but something more at the end.]

It looks to me that, for example, the lexically scoped and no-global-state nature of actor programs means that a lot of code that looks like a transcription of something you'd write in C++ is easy to recognize as being easily compiled using similar techiques.

If your code on the other hand makes use of concurrency then I guess compilation starts to have dealing with scheduling. Probably won't be using a simplistic stack discipline.

If your code has or might have sharing of actors among concurrently running actors, only then do message sends get overheads associated with arbitration of sends.

If you have loosely coupled components (e.g. parts of a system that can be separately updated on the fly) at least you are in the familiar territory where it pays to "be strict in what you trasnmit, tolerant in what you receive".

What happens if this results in the sender and receiver having different types for the same message. Surely any assumption the sender knows the correct types to send will result in a security hole, and so there needs to be a protocol where the types are encoded into the message and the receiver can reject the message if they don't match what it is expecting.

More generally: consider a system that partitions into two set of communicating actors, A and B. And say their is either unilateral or bilateral mistrust. A has to consider that B will malfunction and spew garbage results and/or vice versa.

One suggestive possibility, if Direct Logic is regarded as elements of a logic programming language, is for A to treat the messages from B as containing assertions B makes in what A can think of as "Theory B". Every message B sends is something like a proposition that B says is true in "Theory B".

In that way A winds up with a partial model of Theory B without having to "know" any more details than what B sends along.

Furtheremore, in DL this model of Theory B is scoped under a ⊢_B. So DL provides a (not unique but) simple set of constructs, concepts, and semantics of "containing" a possible inconsistency in Theory B, even while mixing knowledge from theory B with other propositions in a line of (machine executed) proof.

This only works in the case of mutual trust. If the code at one end can change, then the proof is useless as it is about a different version of the code. You need a runtime mechanism to do the type checking of messages sent to remote actors.

This only works in the case of mutual trust. If the code at one end can change, then the proof is useless as it is about a different version of the code.

More generally, the remote code can be wrong for any reason.

Hence slogans like: Distributed and decentralized information systems are pervasively inconsistent.

One question is what kind of system architectures can be robust given that they will (assumably) be pervasively inconsistent?

Another question is what kinds of mathematical and programming tools are useful for those kinds of architecture.

Decrypting and signature verifying are runtime checks.

Yes, that's why they have a performance cost. Generally we can assume everything linked into a single binary is going to be compile time checked and can have security proofs.

What happens if I build a malicious library directly in assembly, I can fake the encryption signature to get at the data, but then treat it locally as different types?

Anything not in the same binary, like other application binaries, libraries etc need to be considered untrusted, just like services provided by another machine would be.

There is a subtle security requirement that seems to be omitted from process calculi, namely, aspects of Actors.

An external party must not be able to automatically cast (as in Java) the address of an Actor to any internal interface that the Actor happens to implement.

The whole thing looks worth reading, and intro section 0.2 Character is especially engaging, about the opposition of observing extensional behavior versus structure of intensional private definition. Many nice remarks summarize pithy notions, such as the only way to observe a system is to communicate with it.

Note opposition is an important idea in presenting ideas clearly, because to say what a thing is, you must also say what it is not. In particular, it's important to identify antithetical aspects that do not belong to members of a group of things you want to define. By default, mixin attributes are considered okay by most people, as long as they are not antagonistic aspects. Identifying antithetical ideas and explaining why they don't get along will improve clarity of whatever you want to define in terms of those ideas.

An amusing application of Murphy's Law to software is that whenever you define an object X as the antithesis of Y, you will come across requirements demanding you masquerade X as a Y, no matter how badly it fits. For example, you might find a way to do X very efficiently, as long as usage context Y never happens. Then folks will ask you to implement Y using X, even after you explain it has nearly pessimal performance despite giving the correct answer.

hi, Please see my plea re: actor discussions.

hi, Please see my plea re: actor discussions.

I have. I will respond to your plea in the separate obnoxious thread that you started.

Here, I am providing some background material to help you or someone else understand the book you say you don't think you understand.

Is that OK with you? To actually provide useful background and context about the book you turned into a topic? Do you mind?

the 'actor' angle on anything on LtU has gone past the breaking point for me. Probably having the first post on this thread be a rather non-sequiter from Hewitt pushing the discussion toward actors put me in a state of mind where any mention of actor by anybody here seems like just feeding trolls. Apologies if we are just very far apart at the moment due to our personal subjective experiences on LtU.

Milner had a good point in his CCS memo. It took a long time to develop an adequate denotational semantics for the Actor Model (what Milner called a "tractable extensional theory"). Because of these difficulties, Milner imposed severe restrictions on CCS that made it inadequate as a general model of (concurrent) computation. To remedy some of these deficiencies in CCS, Milner later developed the pi-calculus (which was still not adequate for general concurrency).

The first adequate denotational semantics for the Actor Model was published here:
Carl Hewitt. (2006). “What is Commitment? Physical, Organizational, and Social” COIN@AAMAS’06. (Revised in Springer Verlag Lecture Notes in Artificial Intelligence. Edited by Javier Vázquez-Salceda and Pablo Noriega. 2007) April 2006.

The issue that must be addressed is how to denotationally model all of the messages that are "in flight."

For convenience of readers:

"What is Commitment? Physical, Organizational, and Social" [Hewitt 2006]

The issue that must be addressed is how to denotationally model all of the messages that are "in flight."

Very funny.

It certainly comes up all the time. I've seen a group of very smart, talented, experienced people sit around a conference table talking about how weird 'servers' are because they never end so how can you prove anything about them, etc. So tools which could help arm people in that regard are appealing.

I guess I should have done a better job saying what I thought was particularly cool about the book. I am less hoping for intro stuff (although that is good, to spread the word, so ok thanks all!) and more about how of late the calculi have been used to prove things about e.g. unbounded nondeterminism. Things that might have seemed impossible for a long time. So that we can have our servers and eat them, too. So I would love to hear from those In The Know what the best state of the art is in process calculi. The particular tome I posted about seems to, according to the author with whom I've been in email contact, fallen into the dusty spaces. Are other approaches as successful in helping those who grok them to prove useful things about concurrency?

I'm sorry to that this might provoke you in the whole bogus anti-Hewittism but I will say that my enthusiasm for nearly everything I now realize he is saying is because I recognize that he has done most of the heavy lifting of formalizing how I and all the best hackers I know have believed about things for decades.

Thomas,

Please don't be discouraged.

Scientific discussions can become highly technical although it is important for practitioners to explain things as simply and intuitively as possible.

Insults and personal attacks are basically irrelevant in the long run although they can degrade LtU and you are right to fight against them.

It's important to concentrate on the argumentation because that's what is important for science and engineering discussion of the issues. Science and engineering are not popularity contests.

Also, as you have discerned, the Actor Model has become the default model of computation partly because it formalizes intuitions and practices that are becoming increasing relevant. Consequently, it provides terminology and principles for addressing many current issues.

Regards,
Carl

PS. Of course, I am not always right ;-)

...and as I have previously written, I very much appreciate the work Hewitt has done as well (including his concerns and activism over the back-door-ness of our society, which is to me even more important than his actor work).

I am also glad that you are seeing this and getting into the depths of it. I'd appreciate you posting posts about what you've learned, in terms and in a writing style that others can engage with.

Unfortunately the style embraced by Hewitt has sort of been doing more harm than good here over time, I personally feel. That's, again, a sad thing since it is probably pushing people away from some good if not great work.

Most of the industrial applications (if that's what you're interested in when you say "servers") of process calculus that I'm aware of have involved model checking rather than proof techniques.

Along the same lines, and unmentioned here so far, is Lamport's work on TLA+ (see here). TLA+ is neither a process calculus nor an Actor-based model. It is a temporal logic for describing the way in which the states of a system evolve. Lamport developed it specifically for specifying and proving things about concurrent systems. But, as with process calculi, although proof is possible it is model-checking that is getting more traction in industry. See, for example, the recent CACM article on Amazon's use of TLA+: How Amazon Web Services Uses Formal Methods by Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff
Communications of the ACM, Vol. 58 No. 4, Pages 66-73.

TLA+ is very low level. Without abstraction, model checking concurrent systems tends to explode with possibilities.

Is there anything more abstract than TLA+ that can be used for model checking?

Yes, state explosion has long been a problem for model-checking. However, there are some interesting techniques (FDR2's compressions, SPIN's partial order reductions, and so on) that can help to combat it. Modern model-checkers can check systems orders of magnitude more complex than those checkable by earlier generations of model checkers.

That said, the best way to combat state explosion is, as you alluded, to choose an appropriate level of abstraction for the model. I agree that many of the examples of TLA+ that Lamport has shown are fairly low-level. But I don't think there's anything inherent in TLA+ that means that you can't operate at higher levels of abstraction. It is, after all, simply a logic over actions. The level of abstraction depends on what you define as "actions" in the system you're modeling. To a certain extent the same is true of other formalisms and model checkers, but seems especially true of TLA+ since it doesn't assume things like a process-based execution model or a specific kind of parallel composition (whereas, for example, model checkers for something like CSP are somewhat constrained by the fact that they are intended to check CSP-like systems).

I haven't looked at it in any detail, but you may be interested in this paper on modeling Actors in TLA+: "ReActor: A notation for the specification of actor systems
and its semantics"

TLA+ incorrectly treats state as global, which is scientifically incorrect in addition to being disastrous for engineering.

PS. Thanks for the link to the ReActor article.

I'm not really all that familiar with TLA+, but my understanding is that it does allow the use of existential quantification to hide variables. I'm not sure whether or not that fully addresses your concerns though. You'll have to take that up with Lamport. Presumably he had his reasons for designing TLA+ the way he did.

If we can somehow represent threads/processes in the type system, we should be able to catch when an actor is potentially accessed from multiple threads, and insert a mutex.

The actor type system does not seem to be able to capture the purity of an actor, so it would need to be enhanced with monads or effects.

If we enhanced the type system in those ways, I could see how a compiler could produce efficient code.

Cacheable Actors are an important special case that can be typed.

For example, that Factorial is cacheable (i.e. caching is allowed) can be be expressed as follows:

Interface Factorial with [N] |••> N.▮

Monads are incompatible with general massive concurrency because they sequence computation steps. Types for borrowing can be awkward for massive concurrency because it can be difficult to keep track of which program is borrowing.

PS. It's probably preferable to mark the messages that cacheable than to mark the messages that are not cacheable although this is not a big deal. Note that a message may be determinate (same result from same request) and still not cacheable because the message can have effects.

PPS. This comment was edited while the following comment by Keean was being composed.

if we represent a pure function:

f :: a -> a

Then we can use a monad to indicate that the function is stateful:

f :: a -> IO a

If we consider these actors:

f.[a] -> a
f.[a] -> IO a

Now the monad means we have to serialise access, from a single thread it is no problem, and from multiple threads we need to insert a mutex.

So your statement "Monads types for borrowing are incompatible with general massive concurrency" is clearly a not a problem. Monads precisely indicate exactly those actors that we need mutex serialised access when used from multiple threads. So far from being incompatible with massive concurrency they provide exactly the type information you need in order to optimise the code appropriately.

Edit: They also provide the distinction between functions/actors that need initialisation (stateful) and those that do not. An alternative would be to consider all functions determinate, and handle stateful functions/actors like C++ function objects (of course the two are related, a stateful object being the fixed point of a record of monadic functions and the state).

Monads allow the type system to automatically track statefullness. Marking functions as cacheable is not safe, as you can get it wrong. Much better to have the type system enforce it.

Also we are not interested in cacheability, but whether access had to be serialised, so the caching annotation does not do exactly what we want in any case.

I don't get the objections to monads with concurrency. If monads are used to contain statefullness they provide exactly the information needed to decide whether an actor needs a mutex for incoming messages (unlike cacheability which does not).

A non-monadic actor would be stateless and side-effectless (pure) and because local variables are stored on the stack (which is thread local) the actor can simply be jumped into (it is safe to use JSR and RTN). In this case passing a message to an actor would reduce to a plain function call.

In the monadic case the sender would need to obtain a lock on the receiver before jumping, but only if multiple threads try and send messages to the actor. One obvious pattern is a stateful actor and a message queue such that the stateful actor is only messaged from a single thread from the queue, but the queue would still need mutex protection. I am not sure yet how to track the number of threads that pass messages.

Cacheable message types must be checked where possible. If an Actor on another computer belonging to someone else has type with a message marked as cacheable, then response can be obtained from cache.

Monads (à la Scott and Strachey) in general mean exponentially slower performance for changing Actors, which is the price of basing all semantics on the lambda calculus.

I kind of see your point. Accessing a mutable store in the IO monad means all mutations have to have a single big mutex. This is not what we want. If however each stateful actor were in its own State monad we don't have this problem. We should get exactly what we want only one thread in each stateful actor at a time.

So it seems to me you might be confusing the IO monad with monads in general.

Monads (à la Scott and Strachey) in general mean exponentially slower performance for changing Actors, which is the price of basing all semantics on the lambda calculus.

Ridiculous. Lambda calculus is a formalism which defines a rewrite system; i.e., it defines a syntax and rewrite rules. Mostly, after that, it is used to study type systems and various confluency properties.

LC doesn't define a rewrite strategy. You can chose a rewrite strategy for LC. Innermost-outermost, call-by-name/value, massively concurrent if you feel like.

The Actor Model seems to have somewhat of a syntax and no associated rewrite calculus. It doesn't have a formal operational model, therefore doesn't let itself be compared to other computational models. A meaningless comparison.

Reversely, it suffices to show that an LC with concurrent evaluation can model a process algebra faithfully. I wouldn't know why you would want to do that, but that at least seems possible.

The language Clean implements a pure functional language based on concurrent rewriting of an LC.

Please provide a syntax, a rewrite calculus, and a rewrite strategy for the Actor Model before making claims.

Te Actor Model has axiomatic and denotational semantics. ActorScript currently has published meta semantics.

Yah. That's what you claim, but I haven't found anything meaningful while scanning your papers. Meta-semantics isn't good enough.

See pages 51-73 of ActorScript for meta semantics.