Feature #10940
closedAlways specify specifications set in job.json
0%
Description
At the moment EMG has some quite tricky rules to select necessary environment model specifications, so that users may be completely unaware about a set of specifications used. I suggest to at least explicitly specify "specifications set" in all job.json and fail early when this is not the case or maybe when the user provides something unsupported (there may be a static list of supported specification sets in job.py). Moreover, rather than using implicit inheritance rules (as far as I understand some environment model specifications are marked as "referenced" and they are used for those specification sets for which they are not provided explicitly), I suggest to explicitly map subsets of specification sets to appropriate specifications. For instance, instead of using something like this:
{
"3.14" : {... "reference": true ...},
"5.5": {...}
}
you can use something like you use for function models:
{
"3.14, 4.17" : {...},
"5.5": {...}
}
BTW, I do believe that spending much effort for development of specifications is strictly necessary for using software model checkers, so it's pretty well to "waste" several minutes to explicitly map specification sets to specifications when adding support for a new specification set.
Updated by Ilja Zakharov over 2 years ago
- Linux kernel has many versions, and it is always essential to set a specification set. But we often develop a single model for a new program to give a try. Maybe it is good to set the version initially, but it is useless until a new version of specifications is prepared.
- A specification file usually contains several descriptions for different specification sets. It is sometimes useful to keep a description for several specification sets, but the most widespread situation is that these descriptions are different. The "reference" entry helps to make some parts of a description to be some kind of default one. Yes, it is not easy to comprehend which specifications will be used for a particular specification set without seeing all specifications in place. But removing reference flags will lead to many copy-paste descriptions, which are difficult to maintain. Such a situation took place recently and was annoying.
Updated by Evgeny Novikov over 2 years ago
Ilja Zakharov wrote in #note-1:
Agree that it is sometimes tricky to understand which specifications are used. Asking for the configuration parameter "specifications set" always is also a good idea. But there are some problems with the proposed solution:
- Linux kernel has many versions, and it is always essential to set a specification set. But we often develop a single model for a new program to give a try. Maybe it is good to set the version initially, but it is useless until a new version of specifications is prepared.
I did not catch. If you are going to develop a new version of specifications, you should develop a new specifications set. Otherwise, nobody will be able to use new specifications. Then one should specify the new specifications set in job.json.
- A specification file usually contains several descriptions for different specification sets. It is sometimes useful to keep a description for several specification sets, but the most widespread situation is that these descriptions are different. The "reference" entry helps to make some parts of a description to be some kind of default one. Yes, it is not easy to comprehend which specifications will be used for a particular specification set without seeing all specifications in place. But removing reference flags will lead to many copy-paste descriptions, which are difficult to maintain. Such a situation took place recently and was annoying.
Please, read my suggestion one more time. I did not propose to copy-paste descriptions and thus have numerous duplicates, but to map specification sets to specifications themselves explicitly.
Updated by Evgeny Novikov over 2 years ago
- Target version changed from 3.3 to 3.4
Updated by Evgeny Novikov over 2 years ago
- Target version changed from 3.4 to 3.5
Updated by Evgeny Novikov over 2 years ago
- Target version changed from 3.5 to 3.4
Updated by Evgeny Novikov over 2 years ago
- Blocks Feature #10932: Output intermediate environment models in a more user-friendly way added
Updated by Evgeny Novikov over 2 years ago
- Status changed from New to Resolved
- Assignee changed from Ilja Zakharov to Evgeny Novikov
I took into account comments from Ilja and did not touch most of logic, but in branch "mandatory-specs-set" one does need to specify a specifications set in job.json. Moreover, I added supported specification sets to the beginning of specification bases, e.g. to presets/jobs/specifications/Linux.json:
{
"specification sets": [
"2.6.33",
"3.14",
"4.6.7",
"4.15",
"4.17",
"5.5"
]
}
The existing work with "reference" entries remains the same, so one will not have a lot of duplicates. BTW, before I did not take into account that particular specification sets can overwrite only vital "reference" entries. That makes their descriptions very concise, but also this complicates building a complete set of entries for a given specification set in mind. This is a tradeoff. Maybe it will be easier to have one default set of entries and allow to add new ones or to overwrite some of them for concrete specification sets if necessary.
Updated by Evgeny Novikov over 2 years ago
- Related to Feature #11106: Define default environment model specifications added
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Closed
After some fixes tests passed, so I merged the branch to master in 50b023900. After update do not forget to specify "specifications set" for copies of old verification jobs without that attribute.
Updated by Evgeny Novikov over 2 years ago
Also, you need to refresh Linux.json with descriptions of requirement specifications for old jobs since now it contains a list of supported specification sets.