search

viperproject / voila

Voila is proof outline checker for fine-grained concurrency verification
Other
1 stars 2 forks source link

Generate interference inference only when necessary #69

Open viper-admin opened 6 years ago

viper-admin commented 6 years ago

Created by @Felalolf on 2018-09-16 14:35

Interference context inference is only required for make-atomic statements and abstract atomic calls. More precisely, only for the updated region of a make-atomic statement and only for the region with special interference context requirements in an abstract atomic call.

Currently, the interference context is inferred for every statement, hence can be reduces to only the aforementioned cases. For this change it might also make sense to inhale the interference context footprint predicate only when necessary, i.e. as shown in the encoding chapter in my master thesis (at the beginning of an abstract atomic statement the predicate permission is inhaled and afterwards exhaled again).

viper-admin commented 5 years ago

@mschwerhoff commented on 2019-01-28 14:14

https://github.com/viperproject/voila/issues/70 was marked as a duplicate of this issue.