Move ProgressModel and RoundingMode to Program#978
Move ProgressModel and RoundingMode to Program#978ThomasHaas wants to merge 2 commits intodevelopmentfrom
Conversation
ThomasHaas
changed the title
… point rounding mode. - Improve registration of TypeConverter for ProgressModel
hernanponcedeleon
force-pushed
the
progSem
branch
from
a9cc5a9 to
341792b
Compare
| @Option(name = ROUNDING_MODE_FLOATS, | ||
| description = "Default rounding mode for floating point operations (default NEAREST_TIES_TO_EVEN).", | ||
| secure = true) | ||
| private FloatingPointRoundingMode floatRoundingMode = NEAREST_TIES_TO_EVEN; | ||
|
|
||
| @Option( | ||
| name = PROGRESSMODEL, | ||
| description = """ | ||
| The progress model to assume: fair (default), hsa, obe, lobe, hsa_obe, unfair. | ||
| To specify progress models per scope, use [<scope>=<progressModel>,...]. | ||
| Defaults to "fair" for unspecified scopes unless "default=<progressModel>" is specified. | ||
| """, | ||
| toUppercase = true) | ||
| private ProgressModel.Hierarchy progressModel = ProgressModel.defaultHierarchy(); | ||
| } |
There was a problem hiding this comment.
While I agree we can argue the floating point rounding mode is part of the semantics of the program this is definitely not the case for the progress model; thus this is not a good place for this option. The later is dependent from the execution environment (in the same way we cannot say that the memory model is part of the program semantics per se).
There was a problem hiding this comment.
While I technically agree that you can argue that the WMM and the ProgressModel are both parts of the environment (to some degree even the rounding mode might be?), I wouldn't necessarily conclude that we must treat them in a similar fashion in Dartagnan.
Generally, the way I see axiomatic program semantics is like this: there is an operational semantics (~a transition system) that models the execution of each thread in a program, and there is the axiomatic layer on top that justifies, in hindsight, each threads actions via rf-edges and possibly other dynamic relations.
In that world, everything that affects the operational part of the semantics I would consider a part of the program, i.e., control-flow, data-flow, rounding modes, speculation behavior, etc.
Then the progress model is considered part of the program as it defines the control-flow behavior of the underlying transition system.
Indeed, this is also reflected in our analyses and the encoding: the ProgramEncoder encodes the progress model, and the ExecutionAnalysis - which we consider a program analysis - reasons about it.
At this point in time, I don't see much benefit in having a third type of "Environment Model" and possibly an "EnvironmentEncoder" to go along with it.
EDIT: Just to make sure: I'm not totally against moving execution environment model elsewhere, possibly back into the VerificationTask class. But at least for now, having the environment model in the Program makes things a bit easier, especially if the model is just a few fields defined by a config.
2 participants
I would probably rename the options to
program.progressModelandprogram.roundingModeFloat.@hernan-poncedeleon would the renaming break some external usages of Dartagnan?