For example, I need a statement like "method X is executed singlethreadedly". What I really mean, is that for the same "this" there is one and only one thread executing statements between lines Y and Z. How does one even express this in terms of "a set of possible states"?
My thinking goes roughly like this: 1. there is a final this.awaitingTermination atomic integer (everyone who sees this, sees the same value of awaitingTermination); 2. all atomic updates never reach zero (a separate theorem); 3. an initial atomic update from 0 to 1 establishes mutual exclusion - those that observe awaitingTermination non-zero, or those who fail to atomically compareAndSet from 0 to 1, are excluded from executing lines Y through Z, by if-condition on line Y.
This is my pragmatic approach. ...But a set of possible states?...
Or: eventually there is either subscription.request, or subscription.cancel. This is definitely a theorem in temporal logic. But how does one express this as "a set of possible states" or "transitions"?
Sometimes just a promise to eventually cancel the subscription is observed - how do you express that? I see a promise, but can't tell if it has already been fulfilled; and yet, I can treat this the same as there is a subscription.cancel (in the past or in the future).
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2020-04-15 09:49 pm (UTC)no subject
Date: 2020-04-18 12:01 pm (UTC)When reasoning about a possibility or impossibility of something, I am using higher level constructs than "a set of states".
no subject
Date: 2020-04-19 09:25 am (UTC)My thinking goes roughly like this: 1. there is a final this.awaitingTermination atomic integer (everyone who sees this, sees the same value of awaitingTermination); 2. all atomic updates never reach zero (a separate theorem); 3. an initial atomic update from 0 to 1 establishes mutual exclusion - those that observe awaitingTermination non-zero, or those who fail to atomically compareAndSet from 0 to 1, are excluded from executing lines Y through Z, by if-condition on line Y.
This is my pragmatic approach. ...But a set of possible states?...
Or: eventually there is either subscription.request, or subscription.cancel. This is definitely a theorem in temporal logic. But how does one express this as "a set of possible states" or "transitions"?
Sometimes just a promise to eventually cancel the subscription is observed - how do you express that? I see a promise, but can't tell if it has already been fulfilled; and yet, I can treat this the same as there is a subscription.cancel (in the past or in the future).