[erlang-questions] semantics hot code swapping in Erlang

[Richard Carlsson]

Austin Anderson wrote:
> I'm wanting to get into researching hot code swapping and was wondering 
> if there was a (formal) semantics for Erlang's behaviour with respects 
> to hot code swapping. I have read the Erlang 4.7.3 Reference Manual 
> which I found through the website, which gives a semi-formal 
> specification, but if there exists either in Erlang or in one of its 
> spin off statically typed versions a formal specification as to how the 
> system behaves with respects to hot code swapping I would appreciate 
> being pointed in its direction.

No, I don't think anyone has written such a document. E.g., Lars-Åke
Fredlund did not include the module system in the semantics in his
thesis ("A Framework for Reasoning about Erlang Code", 2001).

However, the rules are actually rather simple, and it should be
straighforward for someone who knows his formal semantics to model
the hot code swapping in a convincing way, given the informal
specification you have already read.

Basically:

   - A module has a name, some attributes (a map from atoms to terms),
     and some exported functions (a map from atom+arity pairs to funs);
     see also the Core Erlang specification for comparison.

   - There can be at most two loaded versions of a module: the current
     and the old version.

   - A remote call M:F(...), or a call to one of the variants of the
     apply and spawn BIFs, always uses the current module to map the
     module name to the actual function to be called. (In practice,
     the linker does most of the job at load time, so there is no
     lookup overhead at run time for M:F(...) calls.)

   - It is possible to find the set of processes that refer to the
     old version of a module, so that they can be forced to terminate
     before purging the old code (in preparation for loading yet another
     version).

   /Richard