Skip to content

a theoretical model in Redex to investigate stack/heap balance

Notifications You must be signed in to change notification settings

cderici/abstract-machine-interp

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

26 Commits
 
 
 
 
 
 
 
 

Repository files navigation

This is a theoretical model implemented in PLT Redex to investigate the relationship between the stack and the heap when an abstract machine and an interpreter work together.

It includes models for a CEK machine and a stackful (regular recursive) interpreter, both implementing a subset of the Fully Expanded Racket Programs.

The main focus is the memory usage. As the expressions go deeper and deeper, the CEK builds up continuations on the heap (which creates a GC pressure in the real world scenario, e.g., Pycket), while the stackful adds stack frames (in this case to the underlying Redex stack through the recursive meta-function calls).

To share the load between the heap and the stack, we switch back and forth between the two interpreters. While the switch from the CEK to stackful depends on the heap use preference, there are cases where it is mandatory for the stackful to switch to the CEK, such as overflow and continuation capture (because there is no continuation in the stackful).

The investigation is about the trade-offs between these two, and tries to answer questions such as

  • To what extent we can share the load? Can we measure and quantify it?
  • How big is the switch overhead? Can it be bound?
  • What if we had an infinite stack space and only switch because of the continuation captures?

For a related study, see Hieb, Dybvig, Bruggeman, "Representing Control in the Presence of First-Class Continuations" (pdf)

About

a theoretical model in Redex to investigate stack/heap balance

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages