[Feature] Reruned tasks included in the report

[lmandrelli]

Is your feature request related to a problem? Please describe.
When we have reruned task, they are in the rerun/ subdirectory, they are not included in the final report

Describe the solution you'd like
report command should search in the rerun subdirectory

Describe alternatives you've considered
rerun can also overwrite previous execution

[nikstuckenbrock]

Hey @lmandrelli,

I started implementing this feature and ran into a design question I’d love your opinion on.

When reading report data from reruns to include in the final report, do you think it makes more sense to create a separate section for rerun commands, or to merge everything into a single report? My intuition is that merging everything would be more useful overall. That then raises a follow-up question: if merging is the goal, why don’t we do this directly during execution so we don’t need the rerun folder and structure at all?

If we do need to stick with the rerun folder structure but still want to merge reports, there’s another question around task matching. For tasks that exist both in the original run and one or multiple reruns: Do we include only the latest result? Or do we include all results and explicitly mark which tasks are reruns of others?

Let me know what you think.

[lmandrelli]

I used the rerun directory because I wanted to keep tracks of parameters that makes the task fail. It is more in a tamarin modelizer perspective than a way to reproduce the result. We can imagine merging the results in a single table, but clearly saying there are multiple results. The summary table could just display the last result, while in the report, for the specific task, we could display the detail of the previous runs. What do you think about that ?

[cascremers]

Hi both, thanks for this discussion. I want to point out some elements that might influence the design choices.

Determinism

Note that Tamarin is deterministic with respect to its inputs and arguments when it terminates, but runtime and memory usage varies. If we use external constraints to limit time/memory, we might see inconsistent results depending on the system environment and general noise: sometimes we terminate and get something, other times we might not terminate, yielding a "fail". In terms of reproducibility, this means that re-running a specific analysis multiple times can only yield one of 5 patterns: the first three are (1) consistent verified, (2) consistent falsified, (3) consistent fail, and the other two options are (4) a mix of verified and fail, (5) a mix of falsified and fail. It is impossible to get a mix that includes both verified and falsified for the same test and the same version of Tamarin.

Merging results

The question is: what is the objective of the reruns? Is it to establish some average? Or is it to rerun failed attempts in the hope that more system resources are now available within, e.g., the time limit?

In practice, once we get a verified or a falsified result for a specific version of Tamarin and specific settings, we know the status of the lemma (we have a proof or counterexample) even if other runs of the test yield "fail". Thus, one occurrence of verified or falsified should be stored, and for merging, we should only output "fail" if it has failed for all runs. If the multiple runs contain a non-fail result, this should be consistent, and we can report it regardless of the output of the last run.

For multiple runs with consistent output (case 1,2,3) , we could average the time/memory costs, or report the last one. It depends on what the user is interested in.

For multiple runs with inconsistent output (case 4 or 5), it is less clear what the average should be (only over the non-fail cases or over all cases?). If we want there to report a specific value, we should choose the last non-fail output, consistent with what we would report.

[lmandrelli]

Hi @cascremers,

So the main idea of the rerun command was to enable the user to have a simple of reruning failed tasks, because it generates a new json recipe you can tweak rapidly to adjust allowed resources. So it's not a hope of seeing task suceed with the same parameters. Moreover, with the cache system, if you don't change any parameter, you will just hit a cache result directly, so the rerun would be useless.

My idea of keeping the history of failed attempts was to have a simple way for someone who tested different parameters to know which parameter made the task suceed. And as the summary table should show only important information at the beginning of the report, I feel like just keeping the last result found is the best way to display information.

But this feature is mostly oriented in a vision where batch-tamarin would be a helpfull companion to develop your tamarin model. It is shure that this would not be an essential feature in the point of view of the wrapper made to reproduce an experiment.

My main thought if we talk about batch-tamarin as a wrapper to reproduce an experiment is that, when someone would have finished to develop a tamarin model and create a batch-tamarin experiment, they would test their configuration until they have a stable result with hopefully no errors, then clean completely their work and test on a fresh environment to be shure that the experiment will reproduce without problem. So the question of reruning tasks would not be used in the final run, that will be the one used to produce the report.

I don't know if my use case is realistic, but that's what I've done with the project we did in Telecom Nancy with Jannik.
So in the end merging the reruned tasks in the report would be a quality of life enhancement to check if everything is working and what was necessary to make it work, to write the final json recipe that will be given to the end user.

Tell me what do you think about that, and @nikstuckenbrock, if you have any questions or remarks feel free to share your thoughts.

[cascremers]

Hi @lmandrelli and @nikstuckenbrock , thanks, this makes sense to me, then I have another feature in mind :-)
Then let's go ahead with this one as-is, and then we can think about other features later.

[nikstuckenbrock]

Hi @cascremers and @lmandrelli,

I agree with both of your points.

I would therefore proceed with updating the report to include the latest run in the summary and to display a dedicated section for each individual run.

As a potential future enhancement, it might also be useful to automatically generate a recipe based on all available tasks that have been proven or falsified. This would allow one to develop a model using batch-tamarin, keep track of its evolution across all reruns, and ultimately generate a fresh recipe with the required parameters for a final verification step and reproduction.

What do you think?

[lmandrelli]

Yes, it would be an additional quality of life enhancement. When you will be merging all result, this could be achieved pretty easily normally.
Maybe this would need a new command in the CLI to make it really easy to find and use.
I would still recommend to do that on two separate PRs, you can just skip the issue part if you are able to develop it, just tell me which PR should be merged before :)