A Framework for Modeling the Semantics of Synchronous and Asynchronous Procedures with Abstract State Machines

The chapter introduces a framework for modeling the semantics of synchronous and asynchronous procedures using Abstract State Machines (ASMs). It begins with an overview of the importance of formal programming language semantics in applications such as compiler verification and model-checking. The framework focuses on the basic concepts in programming languages, rather than modeling the semantics of a specific language. The main goal is to provide a toolkit for formalizing procedure/function calls and returns. The text discusses non-recursive and recursive procedures, parameter passing mechanisms, functions, and procedures as values. It also explores asynchronous procedures, barrier synchronizations, and the challenges of modeling concurrency. The chapter is organized into sections that introduce the general idea behind programming language semantics, the modeling of procedures and functions, and the specific rules for handling asynchronous procedures. The framework is designed to be modular, allowing for the extension of the language semantics concept by concept, and is applicable to various programming languages with different scoping rules and parameter passing mechanisms.