Click to download audio version
Subodh Sharma is a professor of computer science at IIT Delhi, one of the most prestigious universities in India. While he’s not teaching, Subodh conducts research into the formal verification of distributed systems, and his work on the automated formal verification of smart contacts has drawn international interest.
I called up Subodh because I was looking for someone to explain an approach to writing software called the actor model. The actor model essentially involves sandboxing tasks in such a way that complexity is minimized and all behaviors of a software system can be known under all conditions.
Currently the actor model is applied to the management of telecommunications networks through the Erlang language, and also in secure servers. Understanding the way robust distributed systems are constructed assists in the assessment of platform designs and gives us a view into the future of the ultimate distributed system – the Third Web.
What is the actor model, what are its origins, where is it used
Message Passing Interface (MPI) is very similar – is a standard for communication between processors.
The Actor Model is an abstract model of computation for capturing concurrent interaction in a system.
An actor is a primitive entity of computation.
An independent component of a system with its own address space
Like an object or a task
Actors are not like threads which communicate via shared memory
Actors communicate via explicit messages.
Every actor has an address
Communication is asynchronous
Allowing concurrent execution and message passing
Why is concurrent execution and message passing so challenging?
Concurrency is difficult to reason about because there is so much to take into account.
If the order of arrival of messages from a number of worker processes to a manager process effects the correctness of the manager process output, every possible order of arrival needs to be considered by the programer.
Output determinism means that for a given input to a program the output is always the same.
Non-determinism allows higher performance. Determinism is easier to reason about.
The actor model allows us to have non-deterministic message passing inside a system but maintain deterministic output.
Deterministic messaging involves the sender announcing their intention to send a message and the receiver announcing their intention to receive the message from the sender.
Non-deterministic messaging is where the receiver does not care where the message is coming from
This requires all entities to have names or addresses.
Where is this used?
In telecommunications networks.
Also in secure servers.
And because in blockchains all entities have names/addresses, it is an environment that is ideal for actor model based programming.
Nothing more than software modules
Transactional in nature
Either the transaction meets specifications or it does not
Smart contracts must execute deterministically and be oblivious of the environment in which they are running.
History of the Actor Model
Irene Greif, Gul Agha laid the foundations for the model.
Large community of non CS engineers – aerospace, bioscience, chemical engineering – adopted the MPI for scientific programming. MPI was influenced by the actor model.
Applications existed for concurrency. The complete system needed to be developed for this to emerge.
Subodh’s work on autonomously verified smart contracts
Provided sound guarantees of bug free code
Took smart contract source code & created a semantic preserving translation to an intermediate language that was verification friendly
The translated program preserved all of the behaviors that could have emerged in the original.
Feed this to an automated tool that performs symbolic model checking.
Analyzed smart contracts in generality.
Found many buggy smart contracts.