Formal Modeling of Process Migration

This paper develops a formal model of process migration that describes programs, processes, and the migration of those processes within a migration realm. A migration realm is a group of processors modeled as finite state machines. The model is motivated by a migration application between software and field programmable gate array (FPGA) hardware, and the theorems of the model guide the use of FPGA resources while guaranteeing complete and correct execution of a process. By defining different types of migration realms this paper also develops a migration realm taxonomy.