An abstract machine for asynchronous programs with closures and priority queues

We present the operational semantics of an abstract machine that models computations of event-based asynchronous programs inspired to the Node.js server-side system, a convenient platform for developing Internet of Things applications. The goal of the formal description of Node.js internals is twofold: (1) integrating the existing documentation with a more rigorous semantics and (2) validating widely used programming and transformation patterns by means of mathematical tools like transition systems. Our operational semantics is parametric in the transition system of the host scripting language to mimic the infrastructure of the V8 virtual machine where Javascript code is executed on top of the event-based engine provided by the C++ libuv concurrency library. In this work we focus our attention on priority callback queues, nested callbacks, and closures; these are widely used Node.js programming features which, however, may render programs difficult to understand, manipulate, and validate.