search

viperproject / chalice2silver

Other
0 stars 0 forks source link

Deadlock Avoidance #20

Open viper-admin opened 10 years ago

viper-admin commented 10 years ago

Created by bitbucket user ykass on 2013-10-28 14:29 Last updated on 2014-06-27 09:25

Currently all comparisons of mu-order values and all access permissions to mu fields translate to true. There is no deadlock avoidance mechanism in place.

This is the next major extension of the project.

viper-admin commented 10 years ago

Bitbucket user ykass commented on 2013-10-28 14:30

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

viper-admin commented 10 years ago

Bitbucket user ykass commented on 2013-10-31 14:11

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

viper-admin commented 10 years ago

Bitbucket user ykass commented on 2013-11-01 12:35

Note that mu reordering is not going to be part of the implementation of deadlock avoidance. It is only used in one example in the suite and that example is broken. I don't think we need it.

viper-admin commented 10 years ago

@alexanderjsummers commented on 2013-11-01 13:39

Hi Yannis - just to be sure, have you checked this with Peter? Even if we don't have the examples, this seems to be one of the selling points of their paper on the (admittedly, old) approach.

viper-admin commented 10 years ago

Bitbucket user ykass commented on 2014-06-27 09:25

Deadlock avoidance is part of Christian's "obligations" project, which will also take care of https://github.com/viperproject/chalice2silver/issues/21