Software Engineering

All About That Stack: A Unified Treatment of Regions and Control Effects

by Philipp Schus­ter, Jonathan Im­manuel Brachthäuser, and Klaus Os­ter­mann

Tech­ni­cal re­port. Uni­ver­sity of Tübin­gen, Ger­many, 2021.

This pub­li­ca­tion is re­lated to the Com­pil­ing with Con­tin­u­a­tions re­search pro­ject.

Ab­stract

Ever since the in­cep­tion of Algol have pro­gram­ming lan­guage re­searchers sought good ab­strac­tions to in­spect and ma­nip­u­late stacks while main­tain­ing basic in­vari­ants of pro­gram be­hav­ior. These ab­strac­tions range from pro­ce­dure calls and block struc­ture to re­gion-based re­source man­age­ment and con­trol ef­fects. While all these ab­strac­tions are use­ful and well-de­signed in­di­vid­u­ally, their com­bi­na­tion and in­ter­ac­tion is an open issue. We pre­sent a con­cep­tual frame­work with a novel form of stack ab­strac­tion, in which stacks are de­com­posed into re­gions, moves be­tween stacks are ex­pressed as con­trol ef­fects, and re­la­tion­ships be­tween re­gions are rep­re­sented with sub­re­gion­ing ev­i­dence. We demon­strate and prove that these ab­strac­tions are pow­er­ful enough to ex­press and com­bine re­gion-based re­source man­age­ment and con­trol ef­fect while guar­an­tee­ing re­gion and ef­fect safety in­vari­ants. We also dis­cuss an im­ple­men­ta­tion by means of a com­pi­la­tion to Sys­tem F and val­i­date its util­ity by means of sev­eral stan­dard ex­am­ples.