Allow to specify units for computational resource limits
To enforce computational resource limits we use BenchExec which supported units even in version 1.7 we used before recent changes. Our format allows to specify limits for verification tasks just in bytes and milliseconds which isn't convenient. Limits for verification jobs can be specified in a Bridge form where unit GB is for memory and min is for time (both numbers are floats) - I think that can be remained as is.
To keep backward compatibility I suppose to still interpret limits without units as bytes and milliseconds for memory and time correspondingly.
Updated by Ilja Zakharov about 3 years ago
- Status changed from New to Resolved
- Assignee set to Ilja Zakharov
- Priority changed from High to Urgent
Implemented in core-refactoring.
I have done it as I required this for further refactoring issues. Currently, tasks.json and a configuration of a scheduler node file are allowed to contain values with explicit units for memory- and time-related entries.