PwaUpdate

-------------------------- MODULE PwaUpdate -------------------------- (***************************************************************************) (* Service-worker update flow for an installed PWA in "autoUpdate" mode *) (* with a manual force-check. *) (* *) (* A server holds a deployed app version, bumped by deploys up to *) (* MaxVersion. Each client runs an `active` service worker version and *) (* optionally holds a `waiting` worker (NoSW when absent). An update *) (* check, whether from the periodic timer, visibilitychange, or the *) (* manual force-check button (all identical abstractly, so one Check *) (* action), installs a strictly newer server version into `waiting`. *) (* *) (* There is no prompt and no consent step: skipWaiting + clientsClaim *) (* activate the waiting worker automatically, the page reloads, and *) (* `active` becomes the previously waiting version. The reload is the *) (* step where `active` changes. The UI's build-version stamp always *) (* equals the running `active` version after reload, so it is not a *) (* separate variable. The key property: `active` is monotone, upgrading *) (* only to a version that was first installed as `waiting`. *) (***************************************************************************) EXTENDS Naturals CONSTANTS Clients, \* set of client (browser/installed-PWA) ids, model values MaxVersion \* bound on the number of deployed versions NoSW == 0 \* "no waiting worker" (versions are 1..MaxVersion) VARIABLES serverVersion, \* currently deployed app version on the server active, \* active[c] : SW version client c is running waiting \* waiting[c] : installed waiting SW version, or NoSW vars == <<serverVersion, active, waiting>> ----------------------------------------------------------------------------- Init == /\ serverVersion = 1 /\ active = [c \in Clients |-> 1] /\ waiting = [c \in Clients |-> NoSW] \* A deploy bumps the server's app version. Deploy == /\ serverVersion < MaxVersion /\ serverVersion' = serverVersion + 1 /\ UNCHANGED <<active, waiting>> \* Update check (periodic timer, visibilitychange, or manual force-check): \* a strictly newer server version, not already installed as waiting, \* installs into `waiting`. Check(c) == /\ serverVersion > active[c] /\ serverVersion # waiting[c] /\ waiting' = [waiting EXCEPT ![c] = serverVersion] /\ UNCHANGED <<serverVersion, active>> \* skipWaiting + clientsClaim + reload, fully automatic: the waiting \* worker activates and the page reloads on the new version. This is \* the only step where `active` changes. ActivateReload(c) == /\ waiting[c] # NoSW /\ active' = [active EXCEPT ![c] = waiting[c]] /\ waiting' = [waiting EXCEPT ![c] = NoSW] /\ UNCHANGED serverVersion Next == \/ Deploy \/ \E c \in Clients: Check(c) \/ ActivateReload(c) Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- (* Invariants *) TypeOK == /\ serverVersion \in 1..MaxVersion /\ active \in [Clients -> 1..MaxVersion] /\ waiting \in [Clients -> {NoSW} \cup 1..MaxVersion] \* (1) A client only ever runs a version the server actually deployed. ActiveDeployed == \A c \in Clients: active[c] \in 1..serverVersion \* (2) A waiting worker, when present, is a deployed version strictly \* newer than the one running. WaitingNewer == \A c \in Clients: waiting[c] # NoSW => /\ waiting[c] > active[c] /\ waiting[c] <= serverVersion ----------------------------------------------------------------------------- (* Action property: monotone upgrade. Across every step, a client's active version only ever increases, and only to the previously installed waiting version, which is then cleared: no downgrade, and no skipping to a version that was never installed as waiting. *) MonotoneUpgrade == \A c \in Clients: active'[c] # active[c] => /\ active'[c] > active[c] /\ active'[c] = waiting[c] /\ waiting'[c] = NoSW Safety == [][MonotoneUpgrade]_vars =============================================================================

SPECIFICATION Spec CONSTANTS Clients = {c1, c2} MaxVersion = 3 INVARIANT TypeOK INVARIANT ActiveDeployed INVARIANT WaitingNewer PROPERTY Safety CHECK_DEADLOCK FALSE