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

fridis commented 7 months ago

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 commented 7 months ago

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 commented 5 months ago

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 commented 4 months ago

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

tokiwa-software / fuzion