Loop execution modes in trm_for

[panther03]

This PR adds a field to trm_for indicating the execution mode (sequential, parallel, etc.) Previously a parallel loop was only indicated by an OpenMP pragma annotation, which was not guaranteed to be preserved by transformations, nor was it recognized by the typechecker itself (parallel for correctness was only checked at the time of the transformation).

The intention of adding this field is to track the execution mode of a loop in a way that will be preserved by transformations, so that the typechecker can validate at each step that the requirements of that mode are still correct. This is needed especially for more complicated execution mode proposals like thread for where the typechecker has more work to do to validate the loop (so it does not make sense for transformations to check.)

Since the validation of the parallel for (no sequential invariant) is now performed by the typechecker the transformations don't perform any extra validation as a result of this PR, they just preserve the mode whenever transforming a loop. In cases like loop fusion, they just check that the two loops have the same mode. A loop constructed using the trm_for smart constructor defaults to a Sequential loop.

TODO:

• New unit test that the mode is actually preserved properly? E.g. apply pragma omp for then tile, try to modify contract with sequential invariant?

[charguer]

I checked the diff, it looks great.

One challenge is to make sure that if a loop is tagged parallel then the flag is not dropped unintentionally. On the one hand, sequentializing a loop respects the semantics. On the other hand, it might break performance. I don't know whether there is a good solution, but perhaps we could have a pass on the final output code that lists the loops that could be parallelized but are not marked parallel. An option is to keep track of false-positive would be to introduce in the "sequential-invariant" of the loop contract a dummy resource that says "force-sequential", but the overhead of doing so might be significant.

[panther03]

I checked the diff, it looks great.

One challenge is to make sure that if a loop is tagged parallel then the flag is not dropped unintentionally. On the one hand, sequentializing a loop respects the semantics. On the other hand, it might break performance. I don't know whether there is a good solution, but perhaps we could have a pass on the final output code that lists the loops that could be parallelized but are not marked parallel. An option is to keep track of false-positive would be to introduce in the "sequential-invariant" of the loop contract a dummy resource that says "force-sequential", but the overhead of doing so might be significant.

Makes sense, yeah there is a risk of a bug like that appearing somewhere. Although this PR should not change any printing for the parallel loops, because that is still driven by the pragma annotation, which is different. Those pragma transformations only put the tag for the typechecker, so if I screwed up somewhere here, it would not change the performance. As far as I know, the OMP pragmas are not intended to be preserved across transformations anyway. I suppose there is another problem relating to the pragma attributes not being synced with the loop type if those attributes were to be dropped, but it is not a performance or correctness issue.

I can make an issue for this if it's a big enough concern to keep track of

[Bastacyclop]

@panther03 looks like the CI complains about the output of resources/contracts/loop_mode_check.ml being wrong, maybe the expected file is not up to date ?