Use Effects for resource limitations (heap, stack, time, CPU usage, etc.)

[fridis]

It might make sense to use effects to control resource usage of code, e.g., we could have effects like

• no heap allocation: code is statically checked not to perform any heap allocation.
• heap allocation budget: a given heap allocation budget is enforced
• bounded stack usage: code is statically checked to have a bounded stack usage
• timeout: Execution is stopped if it did not finish before a given point in time is reached
• interruptible: Execution is stopped when another thread requests execution to be interrupted
• total CPU usage: Execution is stopped when CPU usage exceeds a given upper limit
• max. CPU load: Execution is limited to using a given CPU percentage
• CPU affinity: Thread is restricted to run on a given CPU or set of CPUs (via sched_setaffinity)
• other ideas? The idea is that, depending on the resource and the code, static analysis or dynamic checks created by the backend are used to enforce the resource restrictions.

[michaellilltokiwa]

• halts: code is statically check to halt (or take max. n steps) for every possible input. Not sure if useful since this probably is undecidable fairly quickly.

[michaellilltokiwa]

A variant of these effects could be not the imitation of resources but tracking the amount of resources used and give a summary after execution.

[michaellilltokiwa]

In the same vein as halts: koka has a diverge effect. Apparently code may not diverge unless it uses this effect. https://github.com/koka-lang/koka/blob/ce2178d945338edd5a4584b7c89e320816f16a18/doc/spec/tour.kk.md?plain=1#L570