diff --git a/Facett/BLEConnectionHandler.swift b/Facett/BLEConnectionHandler.swift index 9ffb01b..d21186f 100644 --- a/Facett/BLEConnectionHandler.swift +++ b/Facett/BLEConnectionHandler.swift @@ -19,25 +19,23 @@ class BLEConnectionHandler { ErrorHandler.info("Connected to \(cameraName)") - guard let gopro = bleManager.connectingGoPros[uuid] else { - return - } - // Note: Camera name will be stored when we receive the apSSID (serial number) // in BLEResponseHandler after the camera connects and sends status // Notify connection manager to cancel timeout timers bleManager.connectionManager.handleConnectionSuccess(uuid) - // Clear retry status on successful connection on main thread - DispatchQueue.main.async { + // This runs on the CoreBluetooth queue. The lookup used to happen here and + // the move to connectedGoPros in a later main block, so the camera could be + // removed in between and the stale reference reinserted. The whole + // read-decide-write now runs as one block on the state queue. + bleManager.onStateQueue { + guard let gopro = bleManager.connectingGoPros[uuid] else { return } + bleManager.connectionRetryStatus.removeValue(forKey: uuid) // A camera we just connected to is awake, whatever we last told it. bleManager.setDeviceSleeping(uuid, isSleeping: false) - } - // UI updates must happen on main thread - DispatchQueue.main.async { let wasEmpty = bleManager.connectedGoPros.isEmpty bleManager.connectedGoPros[uuid] = gopro // Move to connected list @@ -47,16 +45,17 @@ class BLEConnectionHandler { // Reset initialization flag for new connection gopro.hasReceivedInitialStatus = false + gopro.peripheral.delegate = bleManager + if wasEmpty { bleManager.startKeepAliveTimer() } // Notify that camera is connected bleManager.onCameraConnected?(uuid) - } - gopro.peripheral.delegate = bleManager - gopro.peripheral.discoverServices([BLEManager.Constants.UUIDs.goproService, BLEManager.Constants.UUIDs.goproWiFiService]) + gopro.peripheral.discoverServices([BLEManager.Constants.UUIDs.goproService, BLEManager.Constants.UUIDs.goproWiFiService]) + } } func handleDisconnection(_ peripheral: CBPeripheral, error: Error?) { diff --git a/Facett/BLEManager+StateQueue.swift b/Facett/BLEManager+StateQueue.swift new file mode 100644 index 0000000..9d94a72 --- /dev/null +++ b/Facett/BLEManager+StateQueue.swift @@ -0,0 +1,43 @@ +import Foundation + +extension BLEManager { + + // MARK: - Connection State Access + // + // connectedGoPros / connectingGoPros / discoveredGoPros are `@Published` and + // are read from the CoreBluetooth queue as well as from SwiftUI on main. + // Swift `Dictionary` is not thread-safe, so that is undefined behaviour, and + // a decision made from a value read on one queue can be invalidated before + // the write lands on another. + // + // Dispatching only the WRITES to main does not fix either problem — the read + // still races, and the decision is still stale. What is required is that the + // whole read-decide-write runs as one block on a single queue. Main is that + // queue here, since these properties drive SwiftUI and must be published on + // main regardless. + + /// Run `work` as one atomic block on the state queue (main). + /// + /// Always dispatches, even when the caller is already on main. Running inline + /// on main would be faster, but it makes the order in which blocks land depend + /// on which thread issued them: work dispatched earlier from the CoreBluetooth + /// queue would still be waiting while a later main-thread caller executed + /// immediately, inverting the two. Making each block atomic does not by itself + /// give a consistent order between blocks — routing every block through the + /// same FIFO is what does that. + func onStateQueue(_ work: @escaping () -> Void) { + DispatchQueue.main.async(execute: work) + } + + /// Trap in debug builds if connection state is touched off the state queue. + /// This is what stops the discipline from silently eroding: a new call site + /// that reads a dictionary from a delegate callback fails immediately in + /// development instead of corrupting memory occasionally in the field. + func assertOnStateQueue(_ function: StaticString = #function) { + #if DEBUG + if !Thread.isMainThread { + assertionFailure("Connection state touched off the main queue in \(function)") + } + #endif + } +} diff --git a/Facett/BLEManager.swift b/Facett/BLEManager.swift index 9f644b5..eab932e 100644 --- a/Facett/BLEManager.swift +++ b/Facett/BLEManager.swift @@ -246,6 +246,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph /// Send a command directly (bypasses queue, used by queue processor) private func sendCommandDirectly(_ command: [UInt8], to uuid: UUID, commandName: String, requiresControl: Bool = false) { + assertOnStateQueue() guard let gopro = connectedGoPros[uuid] else { log("Camera not found for direct command: \(commandName)") return @@ -693,6 +694,14 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } func setDateTime(for uuid: UUID) { + // Reached from BLEResponseHandler on the CoreBluetooth queue as well as + // from configureAllDevices, so the guard and the status write below have + // to share one block on the state queue. + onStateQueue { [weak self] in self?.setDateTimeOnStateQueue(for: uuid) } + } + + private func setDateTimeOnStateQueue(for uuid: UUID) { + assertOnStateQueue() guard connectedGoPros[uuid] != nil else { return } let now = Date() @@ -720,9 +729,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph sendCommand(dateTimeCommand, to: uuid, commandName: "set date time") - DispatchQueue.main.async { [weak self] in - self?.connectedGoPros[uuid]?.status.lastTimeSyncDate = now - } + connectedGoPros[uuid]?.status.lastTimeSyncDate = now ErrorHandler.debug("Sent Set Date Time command to \(CameraIdentityManager.shared.getDisplayName(for: uuid)). Date: \(year)-\(month)-\(day) \(hour):\(minute):\(second)") } @@ -743,7 +750,6 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph rssi RSSI: NSNumber ) { let gopro = GoPro(peripheral: peripheral) - guard connectedGoPros[peripheral.identifier] == nil else { return } // Advertisements are always honoured, including from a camera we believe // is asleep. A camera still shutting down and a camera that just woke up @@ -759,7 +765,14 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph let peripheralId = peripheral.identifier let peripheralName = peripheral.name let rssi = RSSI - DispatchQueue.main.async { + + // The already-connected check belongs inside the block with the write it + // guards. Reading it here, on the CoreBluetooth queue, both races the + // dictionary and lets the answer go stale before the insert happens. + onStateQueue { [weak self] in + guard let self = self else { return } + guard self.connectedGoPros[peripheralId] == nil else { return } + let isNew = self.discoveredGoPros[peripheralId] == nil self.addDevice(to: \.discoveredGoPros, gopro: gopro) if isNew { @@ -790,25 +803,34 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph let errorDescription = error?.localizedDescription ?? "unknown error" log("Failed to connect to \(cameraName): \(errorDescription)") - // Log error for crash reporting with enhanced context - CrashReporter.shared.logError( - "BLE Connection Failed", - error: error, - context: [ - "peripheral_name": peripheral.name ?? "Unknown", - "peripheral_id": peripheral.identifier.uuidString, - "peripheral_state": peripheralStateString(peripheral.state), - "error_description": errorDescription, - "error_code": error?._code.description ?? "unknown", - "error_domain": error?._domain ?? "unknown" - ], - appStateContext: createAppStateContext() - ) - let uuid = peripheral.identifier - let currentRetryCount = connectionRetryCount[uuid] ?? 0 + let crashContext: [String: String] = [ + "peripheral_name": peripheral.name ?? "Unknown", + "peripheral_id": peripheral.identifier.uuidString, + "peripheral_state": peripheralStateString(peripheral.state), + "error_description": errorDescription, + "error_code": error?._code.description ?? "unknown", + "error_domain": error?._domain ?? "unknown" + ] + + onStateQueue { [weak self] in + guard let self = self else { return } + + // Logged from here rather than the CoreBluetooth queue: the context + // counts connected and discovered cameras, which is a state read. + CrashReporter.shared.logError( + "BLE Connection Failed", + error: error, + context: crashContext, + appStateContext: self.createAppStateContext() + ) + + // Read the retry count here, on main, rather than snapshotting it on the + // CoreBluetooth queue. Two failures arriving close together would otherwise + // both observe the same value and both write count+1, so the counter would + // never advance and the camera would retry forever instead of being abandoned. + let currentRetryCount = self.connectionRetryCount[uuid] ?? 0 - DispatchQueue.main.async { if let gopro = self.connectingGoPros[uuid] { // Check if we should retry if currentRetryCount < self.maxRetryAttempts { @@ -823,6 +845,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } // Schedule retry after exponential backoff delay + self.connectionRetryTimers[uuid]?.invalidate() self.connectionRetryTimers[uuid] = Timer.scheduledTimer(withTimeInterval: retryDelay, repeats: false) { [weak self] _ in self?.retryConnection(for: uuid) } @@ -832,7 +855,9 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph self.discoveredGoPros[uuid] = gopro // Move back to discovered list self.connectingGoPros.removeValue(forKey: uuid) // Remove from connecting list self.connectionRetryCount.removeValue(forKey: uuid) + self.connectionRetryTimers[uuid]?.invalidate() self.connectionRetryTimers.removeValue(forKey: uuid) + self.connectionAttemptTimers[uuid]?.invalidate() self.connectionAttemptTimers.removeValue(forKey: uuid) self.camerasBeingConnectedFromGroup.remove(uuid) @@ -913,24 +938,33 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph case Constants.UUIDs.wifiAPSSID: ErrorHandler.debug("Processing WiFi AP SSID response for \(peripheral.name ?? "a device")") wifiManager.handleWiFiSSIDResponse(data, for: peripheral) { [weak self] uuid, ssid in - if let gopro = self?.connectedGoPros[uuid] { - self?.wifiManager.updateWiFiSSID(for: uuid, ssid: ssid, gopro: gopro) + // Delivered on the CoreBluetooth queue; the state read and the + // update it feeds must happen together on the state queue. + self?.onStateQueue { + guard let self = self, let gopro = self.connectedGoPros[uuid] else { return } + self.wifiManager.updateWiFiSSID(for: uuid, ssid: ssid, gopro: gopro) } } case Constants.UUIDs.wifiAPPassword: ErrorHandler.debug("Processing WiFi AP Password response for \(peripheral.name ?? "a device")") wifiManager.handleWiFiPasswordResponse(data, for: peripheral) { [weak self] uuid, password in - if let gopro = self?.connectedGoPros[uuid] { - self?.wifiManager.updateWiFiPassword(for: uuid, password: password, gopro: gopro) + // Delivered on the CoreBluetooth queue; the state read and the + // update it feeds must happen together on the state queue. + self?.onStateQueue { + guard let self = self, let gopro = self.connectedGoPros[uuid] else { return } + self.wifiManager.updateWiFiPassword(for: uuid, password: password, gopro: gopro) } } case Constants.UUIDs.wifiAPState: ErrorHandler.debug("Processing WiFi AP State response for \(peripheral.name ?? "a device")") wifiManager.handleWiFiStateResponse(data, for: peripheral) { [weak self] uuid, state in - if let gopro = self?.connectedGoPros[uuid] { - self?.wifiManager.updateWiFiState(for: uuid, state: state, gopro: gopro) + // Delivered on the CoreBluetooth queue; the state read and the + // update it feeds must happen together on the state queue. + self?.onStateQueue { + guard let self = self, let gopro = self.connectedGoPros[uuid] else { return } + self.wifiManager.updateWiFiState(for: uuid, state: state, gopro: gopro) } } @@ -1067,19 +1101,20 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph return } - // Handle the generic case with enhanced logging - let camera = connectedGoPros[uuid] ?? GoPro(peripheral: peripheral) + // Handle the generic case with enhanced logging. + // cameraName is already resolved above, so there is no need to read + // connectedGoPros here -- this runs on the CoreBluetooth queue. let commandName = "Command Type \(commandType)" if success { ErrorHandler.info( - "Command '\(commandName)' succeeded for \(camera.name ?? "Unknown")" + "Command '\(commandName)' succeeded for \(cameraName)" ) ErrorHandler.debug("Command response success for \(cameraName). Command type: \(commandType).") } else { let errorMsg = "Command failed - type \(commandType)" ErrorHandler.error( - "Command '\(commandName)' failed for \(camera.name ?? "Unknown"): \(errorMsg)" + "Command '\(commandName)' failed for \(cameraName): \(errorMsg)" ) log("WARNING: Unhandled command response error for \(cameraName). Command type: \(commandType).") log("Command response error for \(cameraName). Command type: \(commandType).") @@ -1105,17 +1140,13 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph switch (code, value) { case (233, 1): // Claimed control - if let gopro = connectedGoPros[peripheral.identifier] { - gopro.hasControl = true - ErrorHandler.debug("Claimed control") - } + // hasControl is @Published; this runs on the CoreBluetooth queue, so + // publishing from here would update SwiftUI off the main thread. + setHasControl(true, for: peripheral.identifier, reason: "Claimed control") return true case (233, 0): - if let gopro = connectedGoPros[peripheral.identifier] { - gopro.hasControl = false - ErrorHandler.debug("Lost control") - } + setHasControl(false, for: peripheral.identifier, reason: "Lost control") return true case (235, 1): @@ -1585,9 +1616,22 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } private func removeDevice(from collection: ReferenceWritableKeyPath, uuid: UUID) { + assertOnStateQueue() self[keyPath: collection].removeValue(forKey: uuid) } + + /// Update a camera's control flag on the main thread. + /// `hasControl` is `@Published`, but the command responses that change it are + /// delivered on the CoreBluetooth queue. + private func setHasControl(_ hasControl: Bool, for uuid: UUID, reason: String) { + DispatchQueue.main.async { [weak self] in + guard let self = self, let gopro = self.connectedGoPros[uuid] else { return } + gopro.hasControl = hasControl + ErrorHandler.debug(reason) + } + } + private func updateDevice( in collection: ReferenceWritableKeyPath, uuid: UUID, @@ -1731,6 +1775,20 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph DispatchQueue.main.async { self.connectionRetryStatus[uuid] = .connecting self.connectingGoPros[uuid] = gopro + // A connecting camera must not remain in discoveredGoPros: the three + // dictionaries are meant to be mutually exclusive. + self.discoveredGoPros.removeValue(forKey: uuid) + + // CBCentralManager.connect has no implicit timeout, so the first + // attempt needs the same timeout guard the retry path already has. + // Without it a camera can sit in connectingGoPros forever, which + // also permanently prevents scanning from restarting. + self.connectionAttemptTimers[uuid]?.invalidate() + self.connectionAttemptTimers[uuid] = Timer.scheduledTimer( + withTimeInterval: self.connectionTimeout, repeats: false + ) { [weak self] _ in + self?.handleConnectionTimeout(for: uuid) + } } if let cbPeripheral = gopro.peripheral.cbPeripheral { @@ -1762,8 +1820,14 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph centralManager.cancelPeripheralConnection(cbPeripheral) } + // Only the attempt timer is torn down here. The camera stays in + // connectingGoPros so that didFailToConnect's guard still matches — + // removing it first made the deferred failure handler drop the failure + // silently, stranding connectionRetryCount and pinning the UI status. + // Ownership of the connecting -> discovered transition belongs to + // didFailToConnect alone. DispatchQueue.main.async { - self.connectingGoPros.removeValue(forKey: uuid) + self.connectionAttemptTimers[uuid]?.invalidate() self.connectionAttemptTimers.removeValue(forKey: uuid) } @@ -1773,7 +1837,11 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } private func retryConnection(for uuid: UUID) { - guard let gopro = discoveredGoPros[uuid], connectedGoPros[uuid] == nil else { return } + // A camera awaiting retry lives in connectingGoPros, not discoveredGoPros — + // connectToGoPro moves it out of discovered and the retry path leaves it in + // connecting. Guarding on discoveredGoPros here would disable all retries. + guard let gopro = connectingGoPros[uuid] ?? discoveredGoPros[uuid], + connectedGoPros[uuid] == nil else { return } // Check if device was intentionally put to sleep - don't retry if so if deviceStateManager.isDeviceSleeping(uuid) { @@ -1794,6 +1862,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph self.connectingGoPros[uuid] = gopro // Add to connecting list // Set up connection timeout for retry attempt + self.connectionAttemptTimers[uuid]?.invalidate() self.connectionAttemptTimers[uuid] = Timer.scheduledTimer(withTimeInterval: self.connectionTimeout, repeats: false) { [weak self] _ in self?.handleConnectionTimeout(for: uuid) } @@ -1823,15 +1892,22 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } func powerDownGoPro(uuid: UUID) { - guard let gopro = connectedGoPros[uuid] else { return } + // The read, the command, and the removal are one operation. An earlier + // version dispatched only the removal to main and left the lookup on the + // caller's queue, which is the pattern that fixes neither the data race + // nor the stale decision -- the camera can be removed by another path + // between the lookup and the write. + onStateQueue { [weak self] in + guard let self = self, let gopro = self.connectedGoPros[uuid] else { return } - sendPowerDownCommand(to: gopro) + self.sendPowerDownCommand(to: gopro) + self.log("\(gopro.peripheral.name ?? "GoPro") powered down.") - removeDevice(from: \.connectedGoPros, uuid: uuid) - log("\(gopro.peripheral.name ?? "GoPro") powered down.") + self.removeDevice(from: \.connectedGoPros, uuid: uuid) - if connectedGoPros.isEmpty { - stopKeepAliveTimer() + if self.connectedGoPros.isEmpty { + self.stopKeepAliveTimer() + } } } @@ -1930,9 +2006,15 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph ErrorHandler.debug("Discarded \(discarded) timed out partial messages") } - // Query devices on background thread - for uuid in self.connectedGoPros.keys { - self.queryDevice(for: uuid) + // Querying reads connection state, so the decision runs on + // the state queue. Iterating connectedGoPros here on a + // background queue both raced main's writes and could + // mutate the dictionary mid-iteration. The characteristic + // writes themselves still go to bleCommandQueue. + self.onStateQueue { + for uuid in self.connectedGoPros.keys { + self.queryDevice(for: uuid) + } } // Restart timer @@ -2024,6 +2106,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } private func queryDevice(for uuid: UUID) { + assertOnStateQueue() guard let gopro = connectedGoPros[uuid] else { return; } // Check if there are any pending multipart responses for this device @@ -2066,6 +2149,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } private func queryDeviceSetting(for peripheral: PeripheralContainer, command: [UInt8], description: String) { + assertOnStateQueue() guard connectedGoPros[peripheral.identifier]?.hasControl == true else { return } @@ -2131,9 +2215,10 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } func powerDownAllDevices() { - connectedGoPros.forEach {_, gopro in - powerDownGoPro(uuid: gopro.peripheral.identifier) - } + // Iterate a snapshot: powerDownGoPro removes from connectedGoPros, and + // mutating a dictionary while iterating it is undefined behaviour. + let uuids = Array(connectedGoPros.keys) + uuids.forEach { powerDownGoPro(uuid: $0) } } func enableAPAllDevices() { @@ -2229,7 +2314,7 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph // Find cameras that should be connected but aren't let stragglers = targetConnectedCameras.filter { cameraId in - // Camera should be connected if it's discovered but not connected and not currently connecting + // Camera should be connected if it's discovered but not connected and not currently connecting. // A camera the user asked to sleep is excluded: it stays visible and // manually connectable, but must not be reconnected automatically. return discoveredGoPros[cameraId] != nil && @@ -2313,8 +2398,10 @@ class BLEManager: NSObject, ObservableObject, CBCentralManagerDelegate, CBPeriph } } - /// Create app state context for crash reporting + /// Create app state context for crash reporting. + /// Reads connection state, so it must run on the state queue like any other reader. func createAppStateContext(activeGroup: String? = nil) -> AppStateContext { + assertOnStateQueue() return AppStateContext( connectedCameras: connectedGoPros.count, discoveredCameras: discoveredGoPros.count, diff --git a/Facett/BLEPacketReconstructor.swift b/Facett/BLEPacketReconstructor.swift index 51aa64b..9f570b6 100644 --- a/Facett/BLEPacketReconstructor.swift +++ b/Facett/BLEPacketReconstructor.swift @@ -47,7 +47,7 @@ class BLEPacketReconstructor { /// - channelId: the notify characteristic this packet arrived on. Packets /// from different characteristics must not share an accumulation buffer. func processPacket(_ data: Data, peripheralId: String, channelId: String) -> (data: Data, queryID: UInt8)? { - return processPacketLocked(data, peripheralId: peripheralId, channelId: channelId) + return stateQueue.sync { processPacketLocked(data, peripheralId: peripheralId, channelId: channelId) } } private func processPacketLocked(_ data: Data, peripheralId: String, channelId: String) -> (data: Data, queryID: UInt8)? { @@ -77,7 +77,7 @@ class BLEPacketReconstructor { } func clearBuffers() { - clearBuffersLocked() + stateQueue.sync { clearBuffersLocked() } } private func clearBuffersLocked() { @@ -89,7 +89,7 @@ class BLEPacketReconstructor { } func clearBuffers(for peripheralId: String) { - clearBuffersLocked(for: peripheralId) + stateQueue.sync { clearBuffersLocked(for: peripheralId) } } private func clearBuffersLocked(for peripheralId: String) { @@ -104,7 +104,7 @@ class BLEPacketReconstructor { } func getBufferState() -> (buffers: [String: Data], expectedLengths: [String: Int]) { - return (continuationBuffer, expectedMessageLength) + return stateQueue.sync { (continuationBuffer, expectedMessageLength) } } /// Discard buffers that have gone quiet, and report how many were dropped. @@ -116,7 +116,7 @@ class BLEPacketReconstructor { /// data to every connected camera. Truncated data is now dropped outright. @discardableResult func checkTimeouts(timeoutInterval: TimeInterval = 5.0) -> Int { - return checkTimeoutsLocked(timeoutInterval: timeoutInterval) + return stateQueue.sync { checkTimeoutsLocked(timeoutInterval: timeoutInterval) } } private func checkTimeoutsLocked(timeoutInterval: TimeInterval) -> Int { diff --git a/specs/.gitignore b/specs/.gitignore new file mode 100644 index 0000000..3160254 --- /dev/null +++ b/specs/.gitignore @@ -0,0 +1,2 @@ +states/ +*.jar diff --git a/specs/BLEConnection.tla b/specs/BLEConnection.tla new file mode 100644 index 0000000..d653389 --- /dev/null +++ b/specs/BLEConnection.tla @@ -0,0 +1,235 @@ +---------------------------- MODULE BLEConnection ---------------------------- +(***************************************************************************) +(* A TLA+ model of Facett's BLE connection state machine, as implemented *) +(* in Facett/BLEManager.swift and Facett/BLEConnectionHandler.swift. *) +(* *) +(* This spec deliberately models the code AS WRITTEN, not as intended, so *) +(* that TLC produces counterexample traces for the real defects. Each *) +(* modelling choice that mirrors a specific line of Swift is annotated. *) +(* *) +(* Connection state in the app is not an enum -- it is encoded as which of *) +(* three dictionaries a camera currently lives in (BLEManager.swift:160). *) +(* The spec therefore uses three independent sets rather than one *) +(* location variable, so that "camera is in two states at once" is even *) +(* expressible. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Cameras, \* set of camera identities (UUIDs) + MaxRetries, \* BLEManager.maxRetryAttempts (= 3) + QueueBound \* bound on in-flight main-queue blocks, to keep TLC finite + +VARIABLES + discovered, \* BLEManager.discoveredGoPros (keys) + connecting, \* BLEManager.connectingGoPros (keys) + connected, \* BLEManager.connectedGoPros (keys) + retryCount, \* BLEManager.connectionRetryCount + retryTimer, \* BLEManager.connectionRetryTimers (armed?) + attemptTimer, \* BLEManager.connectionAttemptTimers (armed?) + failQueue, \* DispatchQueue.main blocks enqueued by didFailToConnect + failuresProcessed \* ghost: how many retries we have actually scheduled + +vars == <> + +(***************************************************************************) +(* A queued main-queue block carries a SNAPSHOT of retryCount that was *) +(* read earlier, on the CoreBluetooth background queue. This is the *) +(* crux of the lost-update bug: BLEManager.swift:959 reads the count off *) +(* the BLE queue, and BLEManager.swift:966 applies snapshot+1 later on *) +(* main. Modelling the snapshot explicitly is what lets TLC find it. *) +(***************************************************************************) +Block == [cam: Cameras, snapshot: 0..MaxRetries] + +TypeOK == + /\ discovered \subseteq Cameras + /\ connecting \subseteq Cameras + /\ connected \subseteq Cameras + /\ retryTimer \subseteq Cameras + /\ attemptTimer \subseteq Cameras + /\ retryCount \in [Cameras -> 0..MaxRetries] + /\ failuresProcessed \in [Cameras -> Nat] + /\ failQueue \in Seq(Block) + +Init == + /\ discovered = {} + /\ connecting = {} + /\ connected = {} + /\ retryCount = [c \in Cameras |-> 0] + /\ failuresProcessed = [c \in Cameras |-> 0] + /\ retryTimer = {} + /\ attemptTimer = {} + /\ failQueue = <<>> + +----------------------------------------------------------------------------- +\* Environment action: centralManager didDiscover (BLEManager.swift:912) +Discover(c) == + /\ c \notin discovered /\ c \notin connecting /\ c \notin connected + /\ discovered' = discovered \cup {c} + /\ UNCHANGED <> + +(***************************************************************************) +(* connectToGoPro -- BLEManager.swift:1846. *) +(* *) +(* Two faithful details that matter: *) +(* 1. It adds to connectingGoPros (:1871) but does NOT remove from *) +(* discoveredGoPros. That removal happens only on didConnect *) +(* (BLEConnectionHandler.swift:43). *) +(* 2. It does NOT arm a connection-attempt timer. Only retryConnection *) +(* does (BLEManager.swift:1935). *) +(***************************************************************************) +ConnectToGoPro(c) == + /\ c \in discovered + /\ c \notin connecting + /\ c \notin connected + /\ connecting' = connecting \cup {c} + /\ UNCHANGED <> + +\* Environment action: didConnect (BLEConnectionHandler.swift:41-43) +DidConnect(c) == + /\ c \in connecting + /\ connected' = connected \cup {c} + /\ connecting' = connecting \ {c} + /\ discovered' = discovered \ {c} + /\ retryCount' = [retryCount EXCEPT ![c] = 0] + /\ retryTimer' = retryTimer \ {c} + /\ attemptTimer' = attemptTimer \ {c} + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = 0] + /\ UNCHANGED failQueue + +(***************************************************************************) +(* Environment action: didFailToConnect (BLEManager.swift:958-966). *) +(* Reads retryCount on the BLE queue, then defers the decision to main. *) +(***************************************************************************) +DidFail(c) == + /\ c \in connecting + /\ Len(failQueue) < QueueBound + /\ failQueue' = Append(failQueue, [cam |-> c, snapshot |-> retryCount[c]]) + /\ attemptTimer' = attemptTimer \ {c} + /\ UNCHANGED <> + +(***************************************************************************) +(* handleConnectionTimeout -- BLEManager.swift:1880. *) +(* Removes from connectingGoPros (:1904) and THEN re-enters *) +(* didFailToConnect (:1909) -- so by the time the queued block runs, the *) +(* camera is no longer in connectingGoPros. *) +(***************************************************************************) +HandleConnectionTimeout(c) == + /\ c \in attemptTimer + /\ c \in connecting + /\ Len(failQueue) < QueueBound + /\ connecting' = connecting \ {c} + /\ attemptTimer' = attemptTimer \ {c} + /\ failQueue' = Append(failQueue, [cam |-> c, snapshot |-> retryCount[c]]) + /\ UNCHANGED <> + +(***************************************************************************) +(* The deferred main-queue block from didFailToConnect *) +(* (BLEManager.swift:961-1008). Note the guard at :962 -- *) +(* `if let gopro = self.connectingGoPros[uuid]` -- and that the ELSE *) +(* branch is empty: if the camera has left connectingGoPros in the *) +(* meantime, the failure is silently dropped and no state is cleaned up. *) +(***************************************************************************) +ProcessFail == + /\ failQueue # <<>> + /\ LET blk == Head(failQueue) + c == blk.cam + IN /\ failQueue' = Tail(failQueue) + /\ IF c \in connecting + THEN IF blk.snapshot < MaxRetries + THEN \* retry path, BLEManager.swift:966-978 + /\ retryCount' = [retryCount EXCEPT ![c] = blk.snapshot + 1] + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = @ + 1] + /\ retryTimer' = retryTimer \cup {c} + /\ UNCHANGED <> + ELSE \* abandon path, BLEManager.swift:982-987 + /\ connecting' = connecting \ {c} + /\ discovered' = discovered \cup {c} + /\ retryCount' = [retryCount EXCEPT ![c] = 0] + /\ retryTimer' = retryTimer \ {c} + /\ attemptTimer' = attemptTimer \ {c} + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = 0] + /\ UNCHANGED connected + ELSE \* guard failed: block does nothing at all + UNCHANGED <> + +(***************************************************************************) +(* retryConnection -- BLEManager.swift:1913. Guards on discoveredGoPros, *) +(* which still contains the camera (see ConnectToGoPro note 1), then arms *) +(* the attempt timer at :1935. *) +(***************************************************************************) +RetryFire(c) == + /\ c \in retryTimer + /\ retryTimer' = retryTimer \ {c} + /\ IF c \in discovered /\ c \notin connected + THEN /\ connecting' = connecting \cup {c} + /\ attemptTimer' = attemptTimer \cup {c} + ELSE UNCHANGED <> + /\ UNCHANGED <> + +\* didDisconnectPeripheral, non-sleeping path (BLEConnectionHandler.swift:74-80) +Disconnect(c) == + /\ c \in connected + /\ connected' = connected \ {c} + /\ discovered' = discovered \cup {c} + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ ProcessFail + \/ \E c \in Cameras: + \/ Discover(c) \/ ConnectToGoPro(c) \/ DidConnect(c) + \/ DidFail(c) \/ HandleConnectionTimeout(c) + \/ RetryFire(c) \/ Disconnect(c) + +(***************************************************************************) +(* Fairness is asserted ONLY for actions the app itself controls. *) +(* DidConnect and DidFail are CoreBluetooth callbacks -- the radio is *) +(* under no obligation to ever call back, which is precisely why a *) +(* connection attempt needs its own timeout. Leaving them unfair is what *) +(* exposes the missing-timeout liveness bug. *) +(***************************************************************************) +Spec == + /\ Init + /\ [][Next]_vars + /\ WF_vars(ProcessFail) + /\ \A c \in Cameras: + /\ WF_vars(RetryFire(c)) + /\ WF_vars(HandleConnectionTimeout(c)) + +\* Keeps the ghost counter finite so TLC terminates. +StateConstraint == \A c \in Cameras: failuresProcessed[c] <= MaxRetries + 2 + +----------------------------------------------------------------------------- +\* PROPERTIES + +\* A camera should occupy exactly one of the three dictionaries. +MutualExclusion == + \A c \in Cameras: + /\ ~(c \in discovered /\ c \in connecting) + /\ ~(c \in connecting /\ c \in connected) + /\ ~(c \in discovered /\ c \in connected) + +\* A camera must be abandoned after at most MaxRetries scheduled retries. +BoundedRetries == + \A c \in Cameras: failuresProcessed[c] <= MaxRetries + +\* Scanning restarts only when connectingGoPros is empty (BLEManager.swift:2090), +\* so a camera stuck in `connecting` disables discovery for the whole app. +ScanningLive == []<>(connecting = {}) + +\* No camera stays in `connecting` forever. +NoStuckConnecting == \A c \in Cameras: (c \in connecting) ~> (c \notin connecting) + +\* Retry bookkeeping must not outlive the connection attempt it belongs to. +NoOrphanedRetryState == + \A c \in Cameras: + (c \notin connecting /\ c \notin connected) => retryCount[c] = 0 + +============================================================================= diff --git a/specs/BLEConnectionFixed.tla b/specs/BLEConnectionFixed.tla new file mode 100644 index 0000000..fa4324c --- /dev/null +++ b/specs/BLEConnectionFixed.tla @@ -0,0 +1,179 @@ +------------------------- MODULE BLEConnectionFixed ------------------------- +(***************************************************************************) +(* The repaired connection state machine. Same actions as BLEConnection, *) +(* with four changes -- each one corresponding to a concrete code fix: *) +(* *) +(* FIX 1 (MutualExclusion): connectToGoPro moves the camera out of *) +(* discoveredGoPros instead of leaving it in both dictionaries. *) +(* *) +(* FIX 2 (ScanningLive): connectToGoPro arms the connection-attempt *) +(* timer, so the FIRST attempt is bounded, not just retries. *) +(* *) +(* FIX 3 (BoundedRetries): the deferred main-queue block reads *) +(* retryCount LIVE on main rather than using a snapshot taken *) +(* earlier on the CoreBluetooth queue. *) +(* *) +(* FIX 4 (NoOrphanedRetryState): handleConnectionTimeout no longer *) +(* removes the camera from connectingGoPros before re-entering the *) +(* failure path; ownership of that transition belongs to the *) +(* failure handler alone. *) +(* *) +(* Note the coupling: FIX 1 invalidates retryConnection's existing guard *) +(* `guard let gopro = discoveredGoPros[uuid]`, because a retrying camera *) +(* is no longer in discoveredGoPros. The guard must become a check on *) +(* connectingGoPros. Applying FIX 1 without this would silently disable *) +(* all retries. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS Cameras, MaxRetries, QueueBound + +VARIABLES discovered, connecting, connected, retryCount, retryTimer, + attemptTimer, failQueue, failuresProcessed + +vars == <> + +\* The block no longer carries a snapshot -- only the camera identity. +Block == [cam: Cameras] + +TypeOK == + /\ discovered \subseteq Cameras + /\ connecting \subseteq Cameras + /\ connected \subseteq Cameras + /\ retryTimer \subseteq Cameras + /\ attemptTimer \subseteq Cameras + /\ retryCount \in [Cameras -> 0..MaxRetries] + /\ failuresProcessed \in [Cameras -> Nat] + /\ failQueue \in Seq(Block) + +Init == + /\ discovered = {} + /\ connecting = {} + /\ connected = {} + /\ retryCount = [c \in Cameras |-> 0] + /\ failuresProcessed = [c \in Cameras |-> 0] + /\ retryTimer = {} + /\ attemptTimer = {} + /\ failQueue = <<>> + +----------------------------------------------------------------------------- +Discover(c) == + /\ c \notin discovered /\ c \notin connecting /\ c \notin connected + /\ discovered' = discovered \cup {c} + /\ UNCHANGED <> + +\* FIX 1 + FIX 2 +ConnectToGoPro(c) == + /\ c \in discovered + /\ c \notin connecting + /\ c \notin connected + /\ discovered' = discovered \ {c} + /\ connecting' = connecting \cup {c} + /\ attemptTimer' = attemptTimer \cup {c} + /\ UNCHANGED <> + +DidConnect(c) == + /\ c \in connecting + /\ connected' = connected \cup {c} + /\ connecting' = connecting \ {c} + /\ discovered' = discovered \ {c} + /\ retryCount' = [retryCount EXCEPT ![c] = 0] + /\ retryTimer' = retryTimer \ {c} + /\ attemptTimer' = attemptTimer \ {c} + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = 0] + /\ UNCHANGED failQueue + +DidFail(c) == + /\ c \in connecting + /\ Len(failQueue) < QueueBound + /\ failQueue' = Append(failQueue, [cam |-> c]) + /\ attemptTimer' = attemptTimer \ {c} + /\ UNCHANGED <> + +\* FIX 4: stays in `connecting`; the failure handler owns the transition. +HandleConnectionTimeout(c) == + /\ c \in attemptTimer + /\ c \in connecting + /\ Len(failQueue) < QueueBound + /\ attemptTimer' = attemptTimer \ {c} + /\ failQueue' = Append(failQueue, [cam |-> c]) + /\ UNCHANGED <> + +\* FIX 3: reads retryCount live instead of a stale snapshot. +ProcessFail == + /\ failQueue # <<>> + /\ LET c == Head(failQueue).cam + IN /\ failQueue' = Tail(failQueue) + /\ IF c \in connecting + THEN IF retryCount[c] < MaxRetries + THEN /\ retryCount' = [retryCount EXCEPT ![c] = @ + 1] + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = @ + 1] + /\ retryTimer' = retryTimer \cup {c} + /\ UNCHANGED <> + ELSE /\ connecting' = connecting \ {c} + /\ discovered' = discovered \cup {c} + /\ retryCount' = [retryCount EXCEPT ![c] = 0] + /\ retryTimer' = retryTimer \ {c} + /\ attemptTimer' = attemptTimer \ {c} + /\ failuresProcessed' = [failuresProcessed EXCEPT ![c] = 0] + /\ UNCHANGED connected + ELSE UNCHANGED <> + +\* Guard now checks connectingGoPros, per the FIX 1 coupling note above. +RetryFire(c) == + /\ c \in retryTimer + /\ retryTimer' = retryTimer \ {c} + /\ IF c \in connecting /\ c \notin connected + THEN attemptTimer' = attemptTimer \cup {c} + ELSE UNCHANGED attemptTimer + /\ UNCHANGED <> + +Disconnect(c) == + /\ c \in connected + /\ connected' = connected \ {c} + /\ discovered' = discovered \cup {c} + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ ProcessFail + \/ \E c \in Cameras: + \/ Discover(c) \/ ConnectToGoPro(c) \/ DidConnect(c) + \/ DidFail(c) \/ HandleConnectionTimeout(c) + \/ RetryFire(c) \/ Disconnect(c) + +Spec == + /\ Init + /\ [][Next]_vars + /\ WF_vars(ProcessFail) + /\ \A c \in Cameras: + /\ WF_vars(RetryFire(c)) + /\ WF_vars(HandleConnectionTimeout(c)) + +StateConstraint == \A c \in Cameras: failuresProcessed[c] <= MaxRetries + 2 + +----------------------------------------------------------------------------- +MutualExclusion == + \A c \in Cameras: + /\ ~(c \in discovered /\ c \in connecting) + /\ ~(c \in connecting /\ c \in connected) + /\ ~(c \in discovered /\ c \in connected) + +BoundedRetries == \A c \in Cameras: failuresProcessed[c] <= MaxRetries + +ScanningLive == []<>(connecting = {}) + +NoStuckConnecting == \A c \in Cameras: (c \in connecting) ~> (c \notin connecting) + +NoOrphanedRetryState == + \A c \in Cameras: + (c \notin connecting /\ c \notin connected) => retryCount[c] = 0 + +============================================================================= diff --git a/specs/ConnectionConcurrency.tla b/specs/ConnectionConcurrency.tla new file mode 100644 index 0000000..1224b19 --- /dev/null +++ b/specs/ConnectionConcurrency.tla @@ -0,0 +1,190 @@ +------------------------- MODULE ConnectionConcurrency ------------------------- +(***************************************************************************) +(* Which concurrency discipline actually makes BLEManager's shared state *) +(* safe? *) +(* *) +(* BLEManager keeps connection state in three @Published dictionaries. *) +(* CoreBluetooth delegate callbacks run on a background queue *) +(* (BLEManager.swift:652 creates the central with a utility queue), while *) +(* @Published mutations are bounced to main. Roughly 70 accesses across *) +(* nine delegate methods are involved, so the refactor is expensive and *) +(* worth getting right on paper first. *) +(* *) +(* Rather than model all 70 sites, this models the SHAPE they share: a *) +(* read-decide-write over shared state, performed concurrently by a *) +(* CoreBluetooth-queue path and a main-queue path. The retry counter bug *) +(* already fixed in didFailToConnect is exactly this shape, which is why it *) +(* is a fair representative. *) +(* *) +(* Two distinct hazards are checked, because they need different fixes: *) +(* *) +(* NoDataRace - no two threads touching the dictionary at once, one of *) +(* them writing. Swift Dictionary is not thread-safe, so *) +(* this is memory-unsafety, not just a logic error. *) +(* *) +(* NoLostUpdate - no write based on a value read before someone else's *) +(* write landed. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Agents, \* concurrent operations in flight + Discipline \* "current" | "writesOnMain" | "mainAtomic" | "serialQueue" + +VARIABLES + counter, \* the shared state (stands in for connectionRetryCount et al.) + phase, \* per agent: "idle" | "reading" | "held" | "writing" | "done" + snapshot, \* per agent: the value it read + completed \* how many operations have finished + +vars == <> + +MaxOps == Cardinality(Agents) + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Which queue each half of the operation runs on. *) +(* *) +(* "current" - reads happen on the CoreBluetooth queue and writes are *) +(* dispatched to main. This is what the code does today. *) +(* "writesOnMain" - the tempting minimal fix: make sure every WRITE is on *) +(* main, but leave reads where they are. *) +(* "mainAtomic" - the whole read-decide-write runs in one main-queue *) +(* block. *) +(* "serialQueue" - the whole operation runs on one dedicated serial queue *) +(* (equivalently, inside one actor). *) +(***************************************************************************) +ReadQueue == + CASE Discipline = "current" -> "ble" + [] Discipline = "writesOnMain" -> "ble" + [] Discipline = "mainAtomic" -> "main" + [] Discipline = "serialQueue" -> "state" + +WriteQueue == + CASE Discipline = "current" -> "main" + [] Discipline = "writesOnMain" -> "main" + [] Discipline = "mainAtomic" -> "main" + [] Discipline = "serialQueue" -> "state" + +\* Whether read and write are one indivisible block. +Atomic == Discipline \in {"mainAtomic", "serialQueue"} + +QueueOf(p) == + CASE p = "reading" -> ReadQueue + [] p = "held" -> ReadQueue \* holding a snapshot between the halves + [] p = "writing" -> WriteQueue + [] OTHER -> "none" + +\* An agent is touching the dictionary while reading or writing. Holding a +\* snapshot between the two halves is NOT contact -- that is the window in +\* which someone else's write can be lost. +Touching(a) == phase[a] \in {"reading", "writing"} + +----------------------------------------------------------------------------- +TypeOK == + /\ counter \in 0..MaxOps + /\ phase \in [Agents -> {"idle", "reading", "held", "writing", "done"}] + /\ snapshot \in [Agents -> 0..MaxOps] + /\ completed \in 0..MaxOps + +Init == + /\ counter = 0 + /\ phase = [a \in Agents |-> "idle"] + /\ snapshot = [a \in Agents |-> 0] + /\ completed = 0 + +----------------------------------------------------------------------------- +\* A serial queue admits one agent at a time; different queues run in parallel. +QueueFree(q, a) == + \A other \in Agents \ {a}: ~(Touching(other) /\ QueueOf(phase[other]) = q) + +(***************************************************************************) +(* Non-atomic disciplines: read, release, then write later. The gap between *) +(* BeginRead and Write is where the retry counter was lost -- *) +(* BLEManager.swift:959 read on the CoreBluetooth queue and :966 applied *) +(* snapshot+1 inside a later main-queue block. *) +(***************************************************************************) +BeginRead(a) == + /\ ~Atomic + /\ phase[a] = "idle" + /\ QueueFree(ReadQueue, a) + /\ phase' = [phase EXCEPT ![a] = "reading"] + /\ UNCHANGED <> + +EndRead(a) == + /\ ~Atomic + /\ phase[a] = "reading" + /\ snapshot' = [snapshot EXCEPT ![a] = counter] + /\ phase' = [phase EXCEPT ![a] = "held"] + /\ UNCHANGED <> + +BeginWrite(a) == + /\ ~Atomic + /\ phase[a] = "held" + /\ QueueFree(WriteQueue, a) + /\ phase' = [phase EXCEPT ![a] = "writing"] + /\ UNCHANGED <> + +EndWrite(a) == + /\ ~Atomic + /\ phase[a] = "writing" + /\ counter' = snapshot[a] + 1 \* the decision uses the earlier read + /\ phase' = [phase EXCEPT ![a] = "done"] + /\ completed' = completed + 1 + /\ UNCHANGED snapshot + +(***************************************************************************) +(* Atomic disciplines: the whole read-decide-write is one critical section, *) +(* so no other agent can interleave within it. *) +(***************************************************************************) +AtomicBegin(a) == + /\ Atomic + /\ phase[a] = "idle" + /\ QueueFree(ReadQueue, a) + /\ phase' = [phase EXCEPT ![a] = "writing"] + /\ snapshot' = [snapshot EXCEPT ![a] = counter] + /\ UNCHANGED <> + +AtomicEnd(a) == + /\ Atomic + /\ phase[a] = "writing" + /\ counter' = snapshot[a] + 1 + /\ phase' = [phase EXCEPT ![a] = "done"] + /\ completed' = completed + 1 + /\ UNCHANGED snapshot + +----------------------------------------------------------------------------- +Next == + \E a \in Agents: + \/ BeginRead(a) \/ EndRead(a) \/ BeginWrite(a) \/ EndWrite(a) + \/ AtomicBegin(a) \/ AtomicEnd(a) + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +----------------------------------------------------------------------------- +\* PROPERTIES + +(***************************************************************************) +(* Swift's Dictionary is not thread-safe: two threads touching it at once, *) +(* with at least one writing, is undefined behaviour rather than merely a *) +(* stale read. Agents on the same serial queue cannot overlap; agents on *) +(* different queues can. *) +(***************************************************************************) +NoDataRace == + \A a, b \in Agents: + (a # b /\ Touching(a) /\ Touching(b)) + => (QueueOf(phase[a]) = QueueOf(phase[b])) + +(***************************************************************************) +(* Every completed operation must be reflected in the result. This is the *) +(* retry-counter bug generalised: two failures both read n and both write *) +(* n+1, so the counter never advances and the camera retries forever. *) +(***************************************************************************) +NoLostUpdate == + counter >= completed + +\* All operations eventually finish and every one of them counts. +AllOperationsCount == + <>[](completed = MaxOps /\ counter = MaxOps) + +============================================================================= diff --git a/specs/MC_BoundedRetries.cfg b/specs/MC_BoundedRetries.cfg new file mode 100644 index 0000000..7cb1757 --- /dev/null +++ b/specs/MC_BoundedRetries.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1, c2} + MaxRetries = 3 + QueueBound = 3 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT BoundedRetries diff --git a/specs/MC_Conc3.cfg b/specs/MC_Conc3.cfg new file mode 100644 index 0000000..7a38b9b --- /dev/null +++ b/specs/MC_Conc3.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2, op3} + Discipline = "mainAtomic" +INVARIANT TypeOK +INVARIANT NoDataRace +INVARIANT NoLostUpdate +PROPERTY AllOperationsCount diff --git a/specs/MC_ConcLU_current.cfg b/specs/MC_ConcLU_current.cfg new file mode 100644 index 0000000..c4756a9 --- /dev/null +++ b/specs/MC_ConcLU_current.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "current" +INVARIANT TypeOK +INVARIANT NoLostUpdate diff --git a/specs/MC_ConcLU_mainAtomic.cfg b/specs/MC_ConcLU_mainAtomic.cfg new file mode 100644 index 0000000..b97336b --- /dev/null +++ b/specs/MC_ConcLU_mainAtomic.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "mainAtomic" +INVARIANT TypeOK +INVARIANT NoLostUpdate diff --git a/specs/MC_ConcLU_serialQueue.cfg b/specs/MC_ConcLU_serialQueue.cfg new file mode 100644 index 0000000..2af9f79 --- /dev/null +++ b/specs/MC_ConcLU_serialQueue.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "serialQueue" +INVARIANT TypeOK +INVARIANT NoLostUpdate diff --git a/specs/MC_ConcLU_writesOnMain.cfg b/specs/MC_ConcLU_writesOnMain.cfg new file mode 100644 index 0000000..3e2ebf0 --- /dev/null +++ b/specs/MC_ConcLU_writesOnMain.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "writesOnMain" +INVARIANT TypeOK +INVARIANT NoLostUpdate diff --git a/specs/MC_Conc_current.cfg b/specs/MC_Conc_current.cfg new file mode 100644 index 0000000..8b46ad1 --- /dev/null +++ b/specs/MC_Conc_current.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "current" +INVARIANT TypeOK +INVARIANT NoDataRace +INVARIANT NoLostUpdate +PROPERTY AllOperationsCount diff --git a/specs/MC_Conc_mainAtomic.cfg b/specs/MC_Conc_mainAtomic.cfg new file mode 100644 index 0000000..ff0945e --- /dev/null +++ b/specs/MC_Conc_mainAtomic.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "mainAtomic" +INVARIANT TypeOK +INVARIANT NoDataRace +INVARIANT NoLostUpdate +PROPERTY AllOperationsCount diff --git a/specs/MC_Conc_serialQueue.cfg b/specs/MC_Conc_serialQueue.cfg new file mode 100644 index 0000000..e6b8d8a --- /dev/null +++ b/specs/MC_Conc_serialQueue.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "serialQueue" +INVARIANT TypeOK +INVARIANT NoDataRace +INVARIANT NoLostUpdate +PROPERTY AllOperationsCount diff --git a/specs/MC_Conc_writesOnMain.cfg b/specs/MC_Conc_writesOnMain.cfg new file mode 100644 index 0000000..e1a76b2 --- /dev/null +++ b/specs/MC_Conc_writesOnMain.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Agents = {op1, op2} + Discipline = "writesOnMain" +INVARIANT TypeOK +INVARIANT NoDataRace +INVARIANT NoLostUpdate +PROPERTY AllOperationsCount diff --git a/specs/MC_CorrectAttribution.cfg b/specs/MC_CorrectAttribution.cfg new file mode 100644 index 0000000..e4e6d4a --- /dev/null +++ b/specs/MC_CorrectAttribution.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec +CONSTANTS + Peripherals = {pA, pB} + Queries = {q1, q2} + MaxFrags = 2 + MaxClock = 5 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT CorrectAttribution diff --git a/specs/MC_Fixed.cfg b/specs/MC_Fixed.cfg new file mode 100644 index 0000000..69a21a8 --- /dev/null +++ b/specs/MC_Fixed.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1, c2} + MaxRetries = 3 + QueueBound = 3 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT MutualExclusion +INVARIANT BoundedRetries +INVARIANT NoOrphanedRetryState diff --git a/specs/MC_FixedLiveness.cfg b/specs/MC_FixedLiveness.cfg new file mode 100644 index 0000000..db13adb --- /dev/null +++ b/specs/MC_FixedLiveness.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1} + MaxRetries = 3 + QueueBound = 2 +CONSTRAINT StateConstraint +PROPERTY ScanningLive +PROPERTY NoStuckConnecting diff --git a/specs/MC_FragmentIntegrity.cfg b/specs/MC_FragmentIntegrity.cfg new file mode 100644 index 0000000..26ebfc4 --- /dev/null +++ b/specs/MC_FragmentIntegrity.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec +CONSTANTS + Peripherals = {pA, pB} + Queries = {q1, q2} + MaxFrags = 2 + MaxClock = 5 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT FragmentIntegrity diff --git a/specs/MC_Liveness.cfg b/specs/MC_Liveness.cfg new file mode 100644 index 0000000..b6ac2c1 --- /dev/null +++ b/specs/MC_Liveness.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1} + MaxRetries = 3 + QueueBound = 2 +CONSTRAINT StateConstraint +INVARIANT TypeOK +PROPERTY ScanningLive diff --git a/specs/MC_MutualExclusion.cfg b/specs/MC_MutualExclusion.cfg new file mode 100644 index 0000000..ddc3e14 --- /dev/null +++ b/specs/MC_MutualExclusion.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1, c2} + MaxRetries = 3 + QueueBound = 3 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT MutualExclusion diff --git a/specs/MC_NoOrphanedRetryState.cfg b/specs/MC_NoOrphanedRetryState.cfg new file mode 100644 index 0000000..160df94 --- /dev/null +++ b/specs/MC_NoOrphanedRetryState.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Cameras = {c1, c2} + MaxRetries = 3 + QueueBound = 3 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT NoOrphanedRetryState diff --git a/specs/MC_NoPartialDelivery.cfg b/specs/MC_NoPartialDelivery.cfg new file mode 100644 index 0000000..a1e18a7 --- /dev/null +++ b/specs/MC_NoPartialDelivery.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec +CONSTANTS + Peripherals = {pA, pB} + Queries = {q1, q2} + MaxFrags = 2 + MaxClock = 5 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT NoPartialDelivery diff --git a/specs/MC_Order_alwaysAsync.cfg b/specs/MC_Order_alwaysAsync.cfg new file mode 100644 index 0000000..aefb24c --- /dev/null +++ b/specs/MC_Order_alwaysAsync.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec +CONSTANTS + Mode = "alwaysAsync" + MaxOps = 3 +INVARIANT TypeOK +INVARIANT AppliedInIssueOrder +PROPERTY PendingAlwaysDrains diff --git a/specs/MC_Order_inline.cfg b/specs/MC_Order_inline.cfg new file mode 100644 index 0000000..7242cab --- /dev/null +++ b/specs/MC_Order_inline.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec +CONSTANTS + Mode = "inline" + MaxOps = 3 +INVARIANT TypeOK +INVARIANT AppliedInIssueOrder +PROPERTY PendingAlwaysDrains diff --git a/specs/MC_ReassemblyFixed.cfg b/specs/MC_ReassemblyFixed.cfg new file mode 100644 index 0000000..89f8899 --- /dev/null +++ b/specs/MC_ReassemblyFixed.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec +CONSTANTS + Peripherals = {pA, pB} + Channels = {chQuery, chSettings} + Queries = {q1, q2} + MaxFrags = 2 + MaxClock = 5 +CONSTRAINT StateConstraint +INVARIANT TypeOK +INVARIANT FragmentIntegrity +INVARIANT CorrectAttribution +INVARIANT NoPartialDelivery +INVARIANT NoSequenceGap diff --git a/specs/MC_SleepVisibility.cfg b/specs/MC_SleepVisibility.cfg new file mode 100644 index 0000000..42e6a35 --- /dev/null +++ b/specs/MC_SleepVisibility.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +INVARIANT TypeOK +PROPERTY NoNewAutoConnectWhileSleepRequested +PROPERTY NeverPermanentlyInvisibleWhileAwake diff --git a/specs/MC_Sleep_confirmed.cfg b/specs/MC_Sleep_confirmed.cfg new file mode 100644 index 0000000..13528d8 --- /dev/null +++ b/specs/MC_Sleep_confirmed.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT Variant = "confirmed" +INVARIANT TypeOK +PROPERTY NoFightingOwnSleep +PROPERTY NeverPermanentlyInvisibleWhileAwake diff --git a/specs/MC_Sleep_graced.cfg b/specs/MC_Sleep_graced.cfg new file mode 100644 index 0000000..ba26b8c --- /dev/null +++ b/specs/MC_Sleep_graced.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT Variant = "graced" +INVARIANT TypeOK +PROPERTY NoFightingOwnSleep +PROPERTY NeverPermanentlyInvisibleWhileAwake diff --git a/specs/MC_Sleep_naive.cfg b/specs/MC_Sleep_naive.cfg new file mode 100644 index 0000000..6ba7bba --- /dev/null +++ b/specs/MC_Sleep_naive.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT Variant = "naive" +INVARIANT TypeOK +PROPERTY NoFightingOwnSleep +PROPERTY NeverPermanentlyInvisibleWhileAwake diff --git a/specs/MC_Sleep_original.cfg b/specs/MC_Sleep_original.cfg new file mode 100644 index 0000000..9d767c2 --- /dev/null +++ b/specs/MC_Sleep_original.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT Variant = "original" +INVARIANT TypeOK +PROPERTY NoFightingOwnSleep +PROPERTY NeverPermanentlyInvisibleWhileAwake diff --git a/specs/PacketReassembly.tla b/specs/PacketReassembly.tla new file mode 100644 index 0000000..1593216 --- /dev/null +++ b/specs/PacketReassembly.tla @@ -0,0 +1,183 @@ +--------------------------- MODULE PacketReassembly --------------------------- +(***************************************************************************) +(* A TLA+ model of Facett's BLE multi-packet reassembler *) +(* (Facett/BLEPacketReconstructor.swift), together with the delivery step *) +(* in BLEManager.startDeviceQueryTimer that consumes timed-out buffers. *) +(* *) +(* Modelled as written, so TLC produces counterexamples for the real *) +(* defects. Fragments are tagged with the (peripheral, query) they were *) +(* actually sent for, which is what makes misrouting observable -- the *) +(* Swift code has no such tag, which is precisely the problem. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Peripherals, \* connected cameras + Queries, \* query IDs in flight (e.g. 0x12 settings, 0x13 status) + MaxFrags, \* max fragments per message + MaxClock \* bound on the logical clock, to keep TLC finite + +Key == [p: Peripherals, q: Queries] +Frag == [p: Peripherals, q: Queries, idx: 0..MaxFrags] + +NoDelivery == [none |-> TRUE] + +VARIABLES + buffer, \* BLEPacketReconstructor.continuationBuffer + expected, \* BLEPacketReconstructor.expectedMessageLength + active, \* which buffer keys currently exist + lastTime, \* BLEPacketReconstructor.lastPacketTime + clock, \* logical clock feeding lastTime + txOpen, \* camera side: is a message being transmitted for this key + txSent, \* how many fragments of it have been emitted + txTotal, \* how many fragments it will have + lastDelivery \* the most recent message handed to the app + +vars == <> + +Delivery == [key: Key, frags: Seq(Frag), appliedTo: SUBSET Peripherals, + complete: BOOLEAN] + +TypeOK == + /\ active \subseteq Key + /\ buffer \in [Key -> Seq(Frag)] + /\ expected \in [Key -> 0..MaxFrags] + /\ lastTime \in [Key -> 0..MaxClock] + /\ clock \in 0..MaxClock + /\ txOpen \in [Key -> BOOLEAN] + /\ txSent \in [Key -> 0..MaxFrags] + /\ txTotal \in [Key -> 0..MaxFrags] + /\ lastDelivery \in {NoDelivery} \cup Delivery + +Init == + /\ active = {} + /\ buffer = [k \in Key |-> <<>>] + /\ expected = [k \in Key |-> 0] + /\ lastTime = [k \in Key |-> 0] + /\ clock = 0 + /\ txOpen = [k \in Key |-> FALSE] + /\ txSent = [k \in Key |-> 0] + /\ txTotal = [k \in Key |-> 0] + /\ lastDelivery = NoDelivery + +----------------------------------------------------------------------------- +\* Active buffer keys belonging to peripheral p. The Swift code selects these +\* with `$0.hasPrefix(peripheralId)` (BLEPacketReconstructor.swift:171). +ActiveFor(p) == {k \in active: k.p = p} + +(***************************************************************************) +(* handleStartPacket -- BLEPacketReconstructor.swift:126. *) +(* *) +(* Note the unconditional overwrite at :146-148. If a buffer already *) +(* exists for this key, the in-flight partial message is silently *) +(* discarded with no warning. *) +(***************************************************************************) +StartPacket(p, q) == + LET k == [p |-> p, q |-> q] IN + /\ ~txOpen[k] + /\ clock < MaxClock + /\ \E total \in 1..MaxFrags: + /\ txTotal' = [txTotal EXCEPT ![k] = total] + /\ expected' = [expected EXCEPT ![k] = total] + /\ LET frags == <<[p |-> p, q |-> q, idx |-> 0]>> IN + /\ buffer' = [buffer EXCEPT ![k] = frags] + /\ IF 1 >= total + THEN \* single-packet message completes immediately + /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ txSent' = [txSent EXCEPT ![k] = 0] + /\ lastDelivery' = [key |-> k, frags |-> frags, + appliedTo |-> {p}, complete |-> TRUE] + ELSE /\ active' = active \cup {k} + /\ txOpen' = [txOpen EXCEPT ![k] = TRUE] + /\ txSent' = [txSent EXCEPT ![k] = 1] + /\ UNCHANGED lastDelivery + /\ clock' = clock + 1 + /\ lastTime' = [lastTime EXCEPT ![k] = clock + 1] + +(***************************************************************************) +(* handleContinuationPacket -- BLEPacketReconstructor.swift:163. *) +(* *) +(* THE DEFECT: the continuation is routed to whichever buffer for this *) +(* peripheral was touched most recently (:181), because the packet carries *) +(* no correlator the code reads. The 4-bit sequence counter documented at *) +(* BLE_PROTOCOL.md:29 is never parsed, so neither misrouting nor a dropped *) +(* fragment is detectable. *) +(***************************************************************************) +MostRecent(p) == + CHOOSE k \in ActiveFor(p): \A j \in ActiveFor(p): lastTime[k] >= lastTime[j] + +SendContinuation(p, q) == + LET src == [p |-> p, q |-> q] IN + /\ txOpen[src] + /\ txSent[src] < txTotal[src] + /\ ActiveFor(p) # {} + /\ clock < MaxClock + /\ LET dst == MostRecent(p) \* routed by recency, not by q + frag == [p |-> p, q |-> q, idx |-> txSent[src]] + buf == Append(buffer[dst], frag) + IN /\ buffer' = [buffer EXCEPT ![dst] = buf] + /\ txSent' = [txSent EXCEPT ![src] = @ + 1] + /\ IF Len(buf) >= expected[dst] + THEN /\ active' = active \ {dst} + /\ txOpen' = [txOpen EXCEPT ![dst] = FALSE] + /\ lastDelivery' = [key |-> dst, frags |-> buf, + appliedTo |-> {dst.p}, complete |-> TRUE] + ELSE /\ UNCHANGED <> + /\ UNCHANGED lastDelivery + /\ lastTime' = [lastTime EXCEPT ![dst] = clock + 1] + /\ clock' = clock + 1 + /\ UNCHANGED <> + +(***************************************************************************) +(* checkTimeouts (BLEPacketReconstructor.swift:58) feeding the delivery *) +(* loop at BLEManager.swift:2061-2063. *) +(* *) +(* THE DEFECT: the return type is (data, queryID) -- the peripheral half *) +(* of the buffer key is discarded at :68-70. The caller therefore applies *) +(* the partial buffer to EVERY connected camera: *) +(* *) +(* for uuid in self.connectedGoPros.keys { *) +(* self.responseHandler.updateGoProStatus(uuid: uuid, with: ...) *) +(* } *) +(***************************************************************************) +Timeout(k) == + /\ k \in active + /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ lastDelivery' = [key |-> k, + frags |-> buffer[k], + appliedTo |-> Peripherals, \* broadcast to all + complete |-> Len(buffer[k]) >= expected[k]] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ \E p \in Peripherals, q \in Queries: + StartPacket(p, q) \/ SendContinuation(p, q) + \/ \E k \in Key: Timeout(k) + +Spec == Init /\ [][Next]_vars + +StateConstraint == clock <= MaxClock + +----------------------------------------------------------------------------- +\* PROPERTIES + +\* Every fragment in a delivered message must belong to that message. +FragmentIntegrity == + lastDelivery = NoDelivery \/ + \A i \in DOMAIN lastDelivery.frags: + /\ lastDelivery.frags[i].p = lastDelivery.key.p + /\ lastDelivery.frags[i].q = lastDelivery.key.q + +\* A message must be applied only to the camera that sent it. +CorrectAttribution == + lastDelivery = NoDelivery \/ lastDelivery.appliedTo = {lastDelivery.key.p} + +\* A truncated buffer must never be handed to the app as if it were a message. +NoPartialDelivery == + lastDelivery = NoDelivery \/ lastDelivery.complete + +============================================================================= diff --git a/specs/PacketReassemblyFixed.tla b/specs/PacketReassemblyFixed.tla new file mode 100644 index 0000000..adb8174 --- /dev/null +++ b/specs/PacketReassemblyFixed.tla @@ -0,0 +1,192 @@ +------------------------ MODULE PacketReassemblyFixed ------------------------ +(***************************************************************************) +(* The repaired reassembler. Three changes: *) +(* *) +(* FIX 1: buffers are keyed by (peripheral, CHARACTERISTIC) rather than *) +(* (peripheral, queryID). Per the GoPro spec, accumulation is a *) +(* per-characteristic context and each characteristic carries one *) +(* message at a time -- so routing becomes deterministic and the *) +(* "most recently touched buffer" heuristic disappears entirely. *) +(* This is what actually closes FragmentIntegrity: keying by *) +(* queryID invented concurrency that the protocol does not have, *) +(* while ignoring the concurrency it DOES have (0x0077 query *) +(* responses and 0x0075 settings responses arrive independently *) +(* and both fed one buffer set). *) +(* *) +(* FIX 2: the 4-bit continuation sequence counter is parsed and checked. *) +(* A gap discards the message in progress. *) +(* *) +(* FIX 3: timed-out buffers are discarded, never delivered. *) +(* *) +(* Sequence validation alone would NOT have closed FragmentIntegrity: two *) +(* messages interleaved at the same fragment position carry the SAME *) +(* counter value, so the check cannot tell them apart. FIX 1 is doing *) +(* the real work; FIX 2 catches drops and duplicates. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Peripherals, \* connected cameras + Channels, \* notify characteristics (0x0077 query, 0x0075 settings) + Queries, \* query IDs, used only to tag message identity + MaxFrags, + MaxClock + +Key == [p: Peripherals, ch: Channels] +Frag == [p: Peripherals, ch: Channels, q: Queries, idx: 0..MaxFrags] + +NoDelivery == [none |-> TRUE] + +VARIABLES + buffer, expected, active, bufQ, seqNext, + txOpen, txQ, txSent, txTotal, + clock, lastDelivery + +vars == <> + +Delivery == [key: Key, q: Queries, frags: Seq(Frag), + appliedTo: SUBSET Peripherals, complete: BOOLEAN] + +TypeOK == + /\ active \subseteq Key + /\ buffer \in [Key -> Seq(Frag)] + /\ expected \in [Key -> 0..MaxFrags] + /\ bufQ \in [Key -> Queries] + /\ seqNext \in [Key -> 0..MaxFrags] + /\ txOpen \in [Key -> BOOLEAN] + /\ txQ \in [Key -> Queries] + /\ txSent \in [Key -> 0..MaxFrags] + /\ txTotal \in [Key -> 0..MaxFrags] + /\ clock \in 0..MaxClock + /\ lastDelivery \in {NoDelivery} \cup Delivery + +Init == + /\ active = {} + /\ buffer = [k \in Key |-> <<>>] + /\ expected = [k \in Key |-> 0] + /\ bufQ = [k \in Key |-> CHOOSE q \in Queries: TRUE] + /\ seqNext = [k \in Key |-> 0] + /\ txOpen = [k \in Key |-> FALSE] + /\ txQ = [k \in Key |-> CHOOSE q \in Queries: TRUE] + /\ txSent = [k \in Key |-> 0] + /\ txTotal = [k \in Key |-> 0] + /\ clock = 0 + /\ lastDelivery = NoDelivery + +----------------------------------------------------------------------------- +\* A start packet replaces any buffer in progress on this characteristic. +\* (Now an explicit, logged discard rather than a silent overwrite.) +StartPacket(p, ch, q) == + LET k == [p |-> p, ch |-> ch] IN + /\ ~txOpen[k] + /\ clock < MaxClock + /\ \E total \in 1..MaxFrags: + /\ txTotal' = [txTotal EXCEPT ![k] = total] + /\ expected' = [expected EXCEPT ![k] = total] + /\ bufQ' = [bufQ EXCEPT ![k] = q] + /\ txQ' = [txQ EXCEPT ![k] = q] + /\ LET frags == <<[p |-> p, ch |-> ch, q |-> q, idx |-> 0]>> IN + /\ buffer' = [buffer EXCEPT ![k] = frags] + /\ IF 1 >= total + THEN /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ txSent' = [txSent EXCEPT ![k] = 0] + /\ seqNext' = [seqNext EXCEPT ![k] = 0] + /\ lastDelivery' = [key |-> k, q |-> q, frags |-> frags, + appliedTo |-> {p}, complete |-> TRUE] + ELSE /\ active' = active \cup {k} + /\ txOpen' = [txOpen EXCEPT ![k] = TRUE] + /\ txSent' = [txSent EXCEPT ![k] = 1] + /\ seqNext' = [seqNext EXCEPT ![k] = 1] + /\ UNCHANGED lastDelivery + /\ clock' = clock + 1 + +(***************************************************************************) +(* Continuation routing is now deterministic: the buffer for the *) +(* characteristic the packet arrived on. The sequence counter is checked; *) +(* a mismatch discards the message in progress. *) +(***************************************************************************) +SendContinuation(p, ch) == + LET k == [p |-> p, ch |-> ch] IN + /\ txOpen[k] + /\ txSent[k] < txTotal[k] + /\ clock < MaxClock + /\ clock' = clock + 1 + /\ txSent' = [txSent EXCEPT ![k] = @ + 1] + /\ IF k \notin active + THEN \* no buffer in progress -- continuation is dropped + /\ UNCHANGED <> + ELSE LET seq == txSent[k] + frag == [p |-> p, ch |-> ch, q |-> txQ[k], idx |-> seq] + buf == Append(buffer[k], frag) + IN IF seq # seqNext[k] + THEN \* FIX 2: sequence gap -- discard the message in progress + /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ UNCHANGED <> + ELSE /\ buffer' = [buffer EXCEPT ![k] = buf] + /\ seqNext' = [seqNext EXCEPT ![k] = @ + 1] + /\ IF Len(buf) >= expected[k] + THEN /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ lastDelivery' = [key |-> k, q |-> bufQ[k], + frags |-> buf, + appliedTo |-> {p}, + complete |-> TRUE] + ELSE /\ UNCHANGED <> + /\ UNCHANGED lastDelivery + /\ UNCHANGED <> + +\* The radio drops a fragment: the camera advances but nothing arrives. +\* This is what FIX 2 exists to catch. +LoseFragment(p, ch) == + LET k == [p |-> p, ch |-> ch] IN + /\ txOpen[k] + /\ txSent[k] < txTotal[k] + /\ txSent' = [txSent EXCEPT ![k] = @ + 1] + /\ UNCHANGED <> + +\* FIX 3: a timed-out buffer is discarded, not delivered. +Timeout(k) == + /\ k \in active + /\ active' = active \ {k} + /\ txOpen' = [txOpen EXCEPT ![k] = FALSE] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ \E p \in Peripherals, ch \in Channels: + \/ \E q \in Queries: StartPacket(p, ch, q) + \/ SendContinuation(p, ch) + \/ LoseFragment(p, ch) + \/ \E k \in Key: Timeout(k) + +Spec == Init /\ [][Next]_vars + +StateConstraint == clock <= MaxClock + +----------------------------------------------------------------------------- +FragmentIntegrity == + lastDelivery = NoDelivery \/ + \A i \in DOMAIN lastDelivery.frags: + /\ lastDelivery.frags[i].p = lastDelivery.key.p + /\ lastDelivery.frags[i].ch = lastDelivery.key.ch + /\ lastDelivery.frags[i].q = lastDelivery.q + +CorrectAttribution == + lastDelivery = NoDelivery \/ lastDelivery.appliedTo = {lastDelivery.key.p} + +NoPartialDelivery == + lastDelivery = NoDelivery \/ lastDelivery.complete + +\* Fragments of a delivered message are contiguous and in order. +NoSequenceGap == + lastDelivery = NoDelivery \/ + \A i \in DOMAIN lastDelivery.frags: lastDelivery.frags[i].idx = i - 1 + +============================================================================= diff --git a/specs/README.md b/specs/README.md new file mode 100644 index 0000000..f89ff01 --- /dev/null +++ b/specs/README.md @@ -0,0 +1,234 @@ +# Formal specs + +TLA+ models of Facett's BLE layer. + +**Connection state machine** + +- `BLEConnection.tla` — models the code **as currently written** (`BLEManager.swift`, + `BLEConnectionHandler.swift`). All four properties below fail; each failure is a real defect. +- `BLEConnectionFixed.tla` — the same machine with four fixes applied. All properties pass. + These fixes are now applied to `BLEManager.swift`. + +**Sleep tracking** + +- `SleepState.tla` — models the sleep flag against the physical camera, under four + designs selected by the `Variant` constant. **Every one of them fails a property.** +- `SleepVisibility.tla` — the design that works, and what `BLEDeviceStateManager` now does. + +Run: + +```bash +for v in original naive graced confirmed; do + java -cp tla2tools.jar tlc2.TLC -config MC_Sleep_$v.cfg -deadlock SleepState.tla +done +java -cp tla2tools.jar tlc2.TLC -config MC_SleepVisibility.cfg -deadlock SleepVisibility.tla +``` + +| Design | `NoFightingOwnSleep` | `NeverPermanentlyInvisibleWhileAwake` | +|---|---|---| +| `original` — flag never actually set | ✗ | ✓ | +| `naive` — always ignore adverts while flagged | ✓ | ✗ | +| `graced` — ignore only inside a timed window | ✗ | ✓ | +| `confirmed` — clear only after observed silence | ✓ | ✗ | +| `SleepVisibility` — suppress auto-connect only | ✓ | ✓ | + +The impossibility is the point: **a camera still shutting down and a camera that just +woke up emit identical advertisements.** No rule over advertisements plus elapsed time +can separate them, so every such design must choose which way to be wrong — undo the +user's sleep command, or hide the camera forever with no way to reach it (since +`connectToGoPro` requires membership in `discoveredGoPros`). + +`graced` was shipped before this was modelled. TLC found its counterexample in seven +steps: the camera is still advertising when the window closes, so the app re-discovers +it mid-shutdown. The 10-second constant was a guess about hardware timing, and the +design was wrong in principle rather than merely mistuned. + +The way out is to stop inferring. The old guard conflated two concerns — *don't +auto-reconnect a camera the user slept* and *don't show it* — and only the first is +required. Suppressing automatic reconnection alone satisfies both properties with no +assumption about how long shutdown takes. + +One property was deliberately **not** asserted: never auto-reconnecting during +shutdown. TLC shows it conflicts with honouring manual override — the user may connect +mid-shutdown, which clears the flag, and a later auto-reconnect is then correct. Manual +override wins; see the note in `SleepVisibility.tla`. + +**Packet reassembly** + +- `PacketReassembly.tla` — models `BLEPacketReconstructor.swift` plus the delivery loop in + `BLEManager.startDeviceQueryTimer`. All three properties fail. +- `PacketReassemblyFixed.tla` — the repaired design. All four properties pass. + These fixes are now applied to `BLEPacketReconstructor.swift`. + +## Running + +```bash +curl -sSL -o tla2tools.jar \ + https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar + +# as-written — each of these produces a counterexample trace +java -cp tla2tools.jar tlc2.TLC -config MC_MutualExclusion.cfg BLEConnection.tla +java -cp tla2tools.jar tlc2.TLC -config MC_BoundedRetries.cfg BLEConnection.tla +java -cp tla2tools.jar tlc2.TLC -config MC_NoOrphanedRetryState.cfg BLEConnection.tla +java -cp tla2tools.jar tlc2.TLC -config MC_Liveness.cfg BLEConnection.tla + +# fixed — both clean +java -cp tla2tools.jar tlc2.TLC -config MC_Fixed.cfg BLEConnectionFixed.tla +java -cp tla2tools.jar tlc2.TLC -config MC_FixedLiveness.cfg BLEConnectionFixed.tla +``` + +Runtime is a few seconds to ~2 minutes with 2 cameras. Liveness configs use 1 camera to keep +the state graph small; the bugs they expose are per-camera, so this loses no coverage. + +## Connection state concurrency + +`ConnectionConcurrency.tla` answers a design question before the refactor is written: +which discipline actually makes `BLEManager`'s shared dictionaries safe? Roughly 70 +accesses across nine CoreBluetooth delegate methods are involved, so this is expensive +to get wrong. + +```bash +for d in current writesOnMain mainAtomic serialQueue; do + java -cp tla2tools.jar tlc2.TLC -config MC_Conc_$d.cfg -deadlock ConnectionConcurrency.tla +done +``` + +| Discipline | `NoDataRace` | `NoLostUpdate` | +|---|---|---| +| `current` — read on BLE queue, write dispatched to main | ✗ | ✗ | +| `writesOnMain` — ensure every *write* is on main | ✗ | ✗ | +| `mainAtomic` — whole read-decide-write in one main block | ✓ | ✓ | +| `serialQueue` — whole operation on one serial queue / actor | ✓ | ✓ | + +**The result that matters: `writesOnMain` is no better than the status quo.** Moving +writes to the main queue while leaving reads on the CoreBluetooth queue fixes neither +hazard — the read still races a concurrent write (Swift `Dictionary` is not +thread-safe, so that is undefined behaviour, not a stale read), and the decision is +still made from a value that another write can invalidate before it lands. + +What determines safety is whether the whole read-decide-write is **one indivisible +block on a single queue**, not which queue the write happens on. That distinction is +easy to miss when reviewing diffs: a change that adds `DispatchQueue.main.async` around +a mutation looks like a fix and is not one. + +### Ordering between blocks + +`ConnectionConcurrency.tla` establishes that each read-decide-write must be one atomic +block. It says nothing about the order those blocks run in, and the helper written to +implement it made a choice about exactly that: + +```bash +for m in inline alwaysAsync; do + java -cp tla2tools.jar tlc2.TLC -config MC_Order_$m.cfg -deadlock StateQueueOrdering.tla +done +``` + +| `onStateQueue` implementation | `AppliedInIssueOrder` | +|---|---| +| `inline` — run directly when already on main | ✗ violated in 3 steps | +| `alwaysAsync` — always dispatch | ✓ | + +The first version ran `work()` inline when the caller was already on main, to keep +main-thread callers synchronous. TLC inverts two operations immediately: work dispatched +earlier from the CoreBluetooth queue is still waiting while a later main-thread caller +executes right away. + +**Atomicity of each block does not imply a consistent order between blocks.** Routing +every block through the same FIFO is what gives that, so `onStateQueue` now always +dispatches. The cost is that main-thread callers are deferred by a runloop turn; no +caller depends on the effect landing synchronously. + +### Status + +Both disciplines are now applied, each where it fits: + +- **`mainAtomic`** for `BLEManager`'s connection dictionaries. Every CoreBluetooth-queue + path that touched them (`didDiscover`, `didFailToConnect`, `handleConnectionSuccess`, + the WiFi response callbacks, `setDateTime`, the device-query timer) now runs its whole + read-decide-write in one `onStateQueue` block. `assertOnStateQueue()` traps in debug + builds so a new off-queue reader fails immediately rather than corrupting memory + occasionally in the field. +- **`serialQueue`** for `BLEPacketReconstructor`. Its state was touched from the + CoreBluetooth queue (`processPacket`) and the timer queue (`checkTimeouts`) — two + different queues. It does not drive SwiftUI, so a dedicated serial queue is cheaper + than main and keeps packet handling off the main thread. + +The reassembler change is confirmed empirically: a 4,000-iteration concurrent stress +harness runs **0 ThreadSanitizer races**, and the same harness against a build with the +serial queue removed reports `Swift access race in handleStartPacket`. That is the +model's prediction reproduced against real code. + +`BLEManager` has no equivalent empirical check — exercising it needs real BLE traffic, +so its discipline rests on the model plus the debug assertions. + +Two disciplines work. `mainAtomic` is the better fit for connection state: the dictionaries are +`@Published` and drive SwiftUI, so they must be touched on main regardless, and +`serialQueue` would need a second hop to main for every UI update. The model checks +clean at three concurrent agents as well as two, and the codebase contains no +`DispatchQueue.main.sync`, so the usual deadlock risk of a main-only discipline does +not apply. + +## Modelling notes + +Connection state is not an enum in the app — it is encoded as *which of three dictionaries* a +camera lives in (`BLEManager.swift:160`). The spec uses three independent sets rather than one +location variable, so that "camera is in two states at once" is expressible at all. + +CoreBluetooth callbacks (`DidConnect`, `DidFail`) are deliberately left **unfair**: the radio is +under no obligation to ever call back. That is what makes the missing first-attempt timeout show +up as a liveness violation rather than being masked by an unrealistic fairness assumption. + +`failuresProcessed` is a ghost variable — it has no counterpart in the Swift code and exists only +to state `BoundedRetries`. It is reset wherever `retryCount` is reset, so it counts retries within +a single connection episode, not over the app's lifetime. + +## Properties + +| Property | Meaning | As-written result | +|---|---|---| +| `MutualExclusion` | A camera is in exactly one of the three dictionaries | ✗ violated in 3 steps | +| `BoundedRetries` | At most `MaxRetries` retries per connection episode | ✗ violated (lost update) | +| `NoOrphanedRetryState` | Retry bookkeeping does not outlive its attempt | ✗ violated | +| `ScanningLive` | `connectingGoPros` empties infinitely often, so scanning resumes | ✗ violated (stutter) | +| `NoStuckConnecting` | No camera stays in `connecting` forever | ✗ violated | + +## Packet reassembly + +```bash +java -cp tla2tools.jar tlc2.TLC -config MC_FragmentIntegrity.cfg PacketReassembly.tla +java -cp tla2tools.jar tlc2.TLC -config MC_CorrectAttribution.cfg PacketReassembly.tla +java -cp tla2tools.jar tlc2.TLC -config MC_NoPartialDelivery.cfg PacketReassembly.tla +``` + +| Property | Meaning | Result | +|---|---|---| +| `FragmentIntegrity` | Every fragment in a message belongs to that message | ✗ violated in 5 steps | +| `CorrectAttribution` | A message is applied only to the camera that sent it | ✗ violated | +| `NoPartialDelivery` | A truncated buffer is never delivered as a message | ✗ violated | + +Fragments in the model are tagged with the `(peripheral, query)` they were sent for. The Swift +code has no such tag — that absence *is* the bug, and the tag exists only so the model checker +can observe the misrouting. + +The defects, and what closed them: + +1. `FragmentIntegrity` — continuations were routed to whichever buffer for that peripheral was + touched most recently, because nothing in the packet correlated it to a message. + **Fix: key buffers by (peripheral, characteristic).** Accumulation is a per-characteristic + context and each characteristic carries one message at a time, so routing becomes + deterministic. Keying by query ID invented concurrency the protocol does not have, while + ignoring the concurrency it *does* have — query responses (0x0077) and settings responses + (0x0075) stream independently and both fed one buffer set. +2. `NoSequenceGap` — the 4-bit counter documented at `BLE_PROTOCOL.md:29` was never parsed, so a + dropped or duplicated continuation produced a byte-shifted payload that still satisfied the + length check and decoded as plausible-but-wrong TLV. + **Fix: parse and validate the counter; a gap discards the message in progress.** +3. `CorrectAttribution` / `NoPartialDelivery` — `checkTimeouts` dropped the peripheral half of the + buffer key, so `BLEManager` applied one camera's truncated buffer to every connected camera. + **Fix: discard timed-out buffers outright** rather than force-completing them. With nothing + delivered on timeout, the broadcast loop is gone entirely. + +**Sequence validation alone would not have closed `FragmentIntegrity`.** Two messages interleaved +at the same fragment position carry the *same* counter value, so the check cannot tell them apart +— the model checker confirms the property still fails with only fix 2. Re-keying is doing the real +work; counter validation catches drops and duplicates. diff --git a/specs/SleepState.tla b/specs/SleepState.tla new file mode 100644 index 0000000..c4f3538 --- /dev/null +++ b/specs/SleepState.tla @@ -0,0 +1,199 @@ +------------------------------ MODULE SleepState ------------------------------ +(***************************************************************************) +(* A TLA+ model of Facett's camera sleep tracking, covering the physical *) +(* camera as well as the app's belief about it. *) +(* *) +(* Three variants are modelled, selected by the Variant constant, so the *) +(* model checker can show why the shipped design is the one that works: *) +(* *) +(* "original" - setDeviceSleeping wrote through an optional chain into *) +(* dictionaries that nothing populates, so the flag was *) +(* never actually set and isDeviceSleeping always returned *) +(* false. *) +(* *) +(* "naive" - the obvious fix: record the flag and always ignore *) +(* advertisements from a camera believed to be asleep. *) +(* *) +(* "graced" - what is now in BLEDeviceStateManager: ignore *) +(* advertisements only inside the shutdown window, and treat *) +(* a later advertisement as evidence the camera woke. *) +(* *) +(* Time is modelled as the abstract state of the flag ("recent" vs "stale") *) +(* with a fair GraceExpires action, rather than a clock. Using a bounded *) +(* integer clock would let behaviours stutter at the bound and make the *) +(* liveness property vacuous. *) +(***************************************************************************) +EXTENDS Naturals + +CONSTANT Variant \* "original" | "naive" | "graced" + +VARIABLES + cam, \* physical camera: "awake" | "shuttingDown" | "asleep" + appLoc, \* app's view: "absent" | "discovered" | "connected" + flag \* sleep flag: "none" | "recent" (inside grace) | "stale" (past grace) + +vars == <> + +CamStates == {"awake", "shuttingDown", "asleep"} +AppStates == {"absent", "discovered", "connected"} +FlagStates == {"none", "recent", "stale"} + +TypeOK == + /\ cam \in CamStates + /\ appLoc \in AppStates + /\ flag \in FlagStates + +Init == + /\ cam = "awake" + /\ appLoc = "absent" + /\ flag = "none" + +----------------------------------------------------------------------------- +\* A camera radiates advertisements unless it has finished going to sleep. +Advertising == cam \in {"awake", "shuttingDown"} + +(***************************************************************************) +(* shouldIgnoreAdvertisement, per variant. *) +(* *) +(* "original" never ignores, because the flag is never set in the first *) +(* place -- the app immediately re-discovers a camera it just told to *) +(* sleep, and BLEConnectionHandler then schedules a reconnect. *) +(***************************************************************************) +ShouldIgnore(f) == + CASE Variant = "original" -> FALSE + [] Variant = "naive" -> f # "none" + [] Variant = "graced" -> f = "recent" + [] Variant = "confirmed" -> f = "recent" + +\* Flag written when the sleep command is sent. +FlagAfterSleepCommand == + IF Variant = "original" THEN "none" ELSE "recent" + +\* Flag after an advertisement is honoured. Only "graced" treats the +\* advertisement as evidence that the camera woke up. +FlagAfterHonouredAdvert(f) == + IF Variant \in {"graced", "confirmed"} /\ f = "stale" THEN "none" ELSE f + +----------------------------------------------------------------------------- +\* User asks the app to put a connected camera to sleep. +SendSleepCommand == + /\ appLoc = "connected" + /\ cam = "awake" + /\ cam' = "shuttingDown" + /\ flag' = FlagAfterSleepCommand + /\ UNCHANGED appLoc + +\* The camera drops the BLE link as it shuts down. +CameraDisconnects == + /\ appLoc = "connected" + /\ cam # "awake" + \* BLEConnectionHandler moves the camera back to discoveredGoPros unless it + \* believes the camera is sleeping. + /\ appLoc' = IF flag = "none" THEN "discovered" ELSE "absent" + /\ UNCHANGED <> + +\* The camera finishes powering down and stops advertising. +ShutdownCompletes == + /\ cam = "shuttingDown" + /\ cam' = "asleep" + /\ UNCHANGED <> + +(***************************************************************************) +(* The app stops believing the camera is mid-shutdown. *) +(* *) +(* "graced" concludes this purely from elapsed time, which is why it fails *) +(* NoFightingOwnSleep: a camera still advertising when the window closes *) +(* gets re-discovered mid-shutdown. *) +(* *) +(* "confirmed" instead requires having observed the camera go silent, so *) +(* the conclusion is drawn from evidence rather than from a guess about *) +(* how long shutdown takes. *) +(***************************************************************************) +GraceExpires == + /\ flag = "recent" + /\ (Variant = "confirmed" => ~Advertising) + /\ flag' = "stale" + /\ UNCHANGED <> + +\* The user presses the power button on a sleeping camera. +UserWakesCamera == + /\ cam = "asleep" + /\ cam' = "awake" + /\ UNCHANGED <> + +(***************************************************************************) +(* didDiscover. Enabled only when the advertisement will actually be *) +(* honoured, so that an ignored advertisement is modelled as the action *) +(* being disabled rather than as a stuttering step -- otherwise weak *) +(* fairness could be satisfied by doing nothing. *) +(***************************************************************************) +ReceiveAdvertisement == + /\ Advertising + /\ appLoc = "absent" + /\ ~ShouldIgnore(flag) + /\ appLoc' = "discovered" + /\ flag' = FlagAfterHonouredAdvert(flag) + /\ UNCHANGED cam + +\* connectToGoPro requires the camera to be in discoveredGoPros. +Connect == + /\ appLoc = "discovered" + /\ appLoc' = "connected" + /\ flag' = "none" \* a connected camera is awake by definition + /\ UNCHANGED cam + +----------------------------------------------------------------------------- +Next == + \/ SendSleepCommand + \/ CameraDisconnects + \/ ShutdownCompletes + \/ GraceExpires + \/ UserWakesCamera + \/ ReceiveAdvertisement + \/ Connect + +(***************************************************************************) +(* Fairness on everything the app or physics drives. UserWakesCamera is *) +(* deliberately unfair: the user is under no obligation to ever press the *) +(* button, and the liveness property below is conditioned on the camera *) +(* being awake anyway. *) +(***************************************************************************) +Spec == + /\ Init + /\ [][Next]_vars + /\ WF_vars(ReceiveAdvertisement) + /\ WF_vars(GraceExpires) + /\ WF_vars(ShutdownCompletes) + /\ WF_vars(CameraDisconnects) + +----------------------------------------------------------------------------- +\* PROPERTIES + +(***************************************************************************) +(* The app must not undo its own sleep command: while the camera is still *) +(* shutting down, it must not reappear as a connectable camera. *) +(* Violated by "original", where the flag is never set. *) +(***************************************************************************) +NoFightingOwnSleep == + [](cam = "shuttingDown" => appLoc # "discovered") + +(***************************************************************************) +(* An awake camera must eventually become reachable. A camera kept out of *) +(* discoveredGoPros can never be connected to, because connectToGoPro *) +(* requires it to be there -- so believing it asleep forever makes it *) +(* permanently invisible with no way for the user to recover. *) +(* Violated by "naive", which never clears the flag. *) +(***************************************************************************) +AwakeCameraBecomesReachable == + (cam = "awake" /\ appLoc = "absent") ~> (appLoc # "absent") + +\* Same claim as SleepVisibility's, stated over this model, to confirm the +\* property discriminates between the designs rather than passing vacuously. +NeverPermanentlyInvisibleWhileAwake == + ~<>[](cam = "awake" /\ appLoc = "absent") + +\* Sanity: the app never believes a camera is asleep while connected to it. +NoSleepingWhileConnected == + [](appLoc = "connected" => flag # "recent") + +============================================================================= diff --git a/specs/SleepVisibility.tla b/specs/SleepVisibility.tla new file mode 100644 index 0000000..0a393ad --- /dev/null +++ b/specs/SleepVisibility.tla @@ -0,0 +1,172 @@ +---------------------------- MODULE SleepVisibility ---------------------------- +(***************************************************************************) +(* SleepState.tla shows that no rule based on advertisements plus time can *) +(* satisfy both requirements at once: *) +(* *) +(* - "graced" (clear the belief after a fixed window) re-discovers a *) +(* camera that is still shutting down, undoing the sleep. *) +(* - "confirmed" (clear it only after observed silence) leaves a camera *) +(* that woke quickly permanently invisible. *) +(* *) +(* A camera that is still shutting down and a camera that just woke up emit *) +(* identical advertisements, so the app cannot tell them apart. Any rule *) +(* must therefore choose which way to be wrong. *) +(* *) +(* This module models the way out: stop trying to infer the answer. The *) +(* original guard conflated two separate concerns -- *) +(* *) +(* (a) do not AUTO-reconnect a camera the user just put to sleep *) +(* (b) do not HIDE a camera from the user *) +(* *) +(* Only (a) is actually required. Keeping the camera visible while *) +(* suppressing only automatic reconnection satisfies both requirements with *) +(* no assumption about how long shutdown takes. *) +(***************************************************************************) +EXTENDS Naturals + +VARIABLES + cam, \* "awake" | "shuttingDown" | "asleep" + visible, \* is the camera in discoveredGoPros (user can tap to connect)? + conn, \* "none" | "auto" | "manual" -- how the app connected, if at all + flag \* app believes the user asked this camera to sleep + +vars == <> + +TypeOK == + /\ cam \in {"awake", "shuttingDown", "asleep"} + /\ visible \in BOOLEAN + /\ conn \in {"none", "auto", "manual"} + /\ flag \in BOOLEAN + +Init == + /\ cam = "awake" + /\ visible = FALSE + /\ conn = "none" + /\ flag = FALSE + +Advertising == cam \in {"awake", "shuttingDown"} + +----------------------------------------------------------------------------- +\* Advertisements are ALWAYS honoured now: visibility is never suppressed. +ReceiveAdvertisement == + /\ Advertising + /\ ~visible + /\ visible' = TRUE + /\ UNCHANGED <> + +\* A camera that has gone quiet eventually drops off the discovered list. +AdvertisementsCease == + /\ ~Advertising + /\ visible + /\ visible' = FALSE + /\ UNCHANGED <> + +(***************************************************************************) +(* Automatic reconnection -- scheduleReconnectIfNeeded, straggler retries, *) +(* connect-all. This is the ONLY thing the sleep flag suppresses. *) +(***************************************************************************) +AutoConnect == + /\ visible + /\ conn = "none" + /\ ~flag \* suppressed while the user wants it asleep + /\ conn' = "auto" + /\ UNCHANGED <> + +(***************************************************************************) +(* The user taps the camera. Always allowed -- this is the escape hatch *) +(* that the previous designs removed, and it also clears the flag, since *) +(* an explicit connect request overrides an earlier sleep request. *) +(***************************************************************************) +ManualConnect == + /\ visible + /\ conn = "none" + /\ conn' = "manual" + /\ flag' = FALSE + /\ UNCHANGED <> + +SendSleepCommand == + /\ conn # "none" + /\ cam = "awake" + /\ cam' = "shuttingDown" + /\ flag' = TRUE + /\ UNCHANGED <> + +CameraDisconnects == + /\ conn # "none" + /\ cam # "awake" + /\ conn' = "none" + /\ UNCHANGED <> + +ShutdownCompletes == + /\ cam = "shuttingDown" + \* The BLE link cannot survive the camera powering off, so the + \* disconnect necessarily precedes the camera being fully asleep. + /\ conn = "none" + /\ cam' = "asleep" + /\ UNCHANGED <> + +UserWakesCamera == + /\ cam = "asleep" + /\ cam' = "awake" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ ReceiveAdvertisement \/ AdvertisementsCease + \/ AutoConnect \/ ManualConnect + \/ SendSleepCommand \/ CameraDisconnects + \/ ShutdownCompletes \/ UserWakesCamera + +Spec == + /\ Init + /\ [][Next]_vars + /\ WF_vars(ReceiveAdvertisement) + /\ WF_vars(CameraDisconnects) + /\ WF_vars(ShutdownCompletes) + +----------------------------------------------------------------------------- +\* PROPERTIES + +(***************************************************************************) +(* These are action properties, not invariants. A plain invariant such as *) +(* [](flag => conn # "auto") also flags the benign case where the app was *) +(* already auto-connected and the user THEN asked for sleep -- that *) +(* connection predates the request and is not a violation. What matters is *) +(* that the app never ESTABLISHES a new automatic connection against the *) +(* user's stated wish. *) +(***************************************************************************) + +\* Never start an automatic connection while the user wants the camera asleep. +NoNewAutoConnectWhileSleepRequested == + [][ (conn = "none" /\ conn' = "auto") => ~flag ]_vars + +(***************************************************************************) +(* NOTE: a stronger property -- *) +(* *) +(* [][ (conn = "none" /\ conn' = "auto") => cam # "shuttingDown" ]_vars *) +(* *) +(* -- is NOT checked here, because it is genuinely too strong. TLC finds a *) +(* trace where the user manually connects while the camera is still *) +(* shutting down (which clears the flag, since an explicit connect *) +(* overrides an earlier sleep request), the camera then drops the link, *) +(* and the app auto-reconnects. That is correct behaviour: the user's most *) +(* recent expressed intent was "connect". Honouring manual override and *) +(* never reconnecting mid-shutdown are incompatible, and override wins. *) +(***************************************************************************) + +(***************************************************************************) +(* An awake camera always becomes visible again, with NO assumption about *) +(* how long shutdown takes -- visibility is never suppressed, so the user *) +(* always retains a way to reach the camera. This is what both timing-based *) +(* designs had to trade away. *) +(***************************************************************************) +(* Leads-to is the wrong operator here: the app may legitimately send a new *) +(* sleep command in the window between the camera waking and its first *) +(* advertisement being processed, which makes (cam = "awake") ~> visible *) +(* fail for reasons that are not defects. What must never happen is the *) +(* camera being awake and invisible FOREVER -- the permanent-invisibility *) +(* trap that the naive design falls into. *) +NeverPermanentlyInvisibleWhileAwake == + ~<>[](cam = "awake" /\ ~visible) + +============================================================================= diff --git a/specs/StateQueueOrdering.tla b/specs/StateQueueOrdering.tla new file mode 100644 index 0000000..e3ddb6e --- /dev/null +++ b/specs/StateQueueOrdering.tla @@ -0,0 +1,100 @@ +--------------------------- MODULE StateQueueOrdering --------------------------- +(***************************************************************************) +(* Does `onStateQueue` preserve the order in which operations were issued? *) +(* *) +(* ConnectionConcurrency.tla establishes that the whole read-decide-write *) +(* must run as one block on one queue. It says nothing about the ORDER in *) +(* which those blocks run relative to each other, and the helper introduced *) +(* to implement that discipline makes a choice about exactly that: *) +(* *) +(* func onStateQueue(_ work: @escaping () -> Void) { *) +(* if Thread.isMainThread { work() } // inline *) +(* else { DispatchQueue.main.async(execute: work) } *) +(* } *) +(* *) +(* Running inline when already on main was chosen to keep main-thread *) +(* callers synchronous. That reasoning optimises for synchronicity at the *) +(* possible cost of global ordering, which is worth checking rather than *) +(* assuming: work issued earlier from the CoreBluetooth queue is still *) +(* queued while a later main-thread caller executes immediately. *) +(* *) +(* "inline" - the shipped helper. *) +(* "alwaysAsync" - always dispatch, so every block goes through one FIFO. *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANTS + Mode, \* "inline" | "alwaysAsync" + MaxOps \* bound on operations issued, to keep TLC finite + +VARIABLES + issued, \* operations in the order they were issued (real-time order) + pending, \* operations dispatched to main and not yet run + applied, \* operations in the order their effects actually landed + nextId + +vars == <> + +Ops == 1..MaxOps + +TypeOK == + /\ issued \in Seq(Ops) + /\ pending \in Seq(Ops) + /\ applied \in Seq(Ops) + /\ nextId \in 1..(MaxOps + 1) + +Init == + /\ issued = <<>> + /\ pending = <<>> + /\ applied = <<>> + /\ nextId = 1 + +----------------------------------------------------------------------------- +(***************************************************************************) +(* A caller issues a state operation from one of the two queues. Under *) +(* "inline" a main-thread caller's work lands immediately, overtaking *) +(* anything the CoreBluetooth queue dispatched earlier. *) +(***************************************************************************) +Issue(q) == + /\ nextId <= MaxOps + /\ issued' = Append(issued, nextId) + /\ nextId' = nextId + 1 + /\ IF Mode = "inline" /\ q = "main" + THEN /\ applied' = Append(applied, nextId) + /\ UNCHANGED pending + ELSE /\ pending' = Append(pending, nextId) + /\ UNCHANGED applied + +\* The main queue runs the next dispatched block. +Drain == + /\ pending # <<>> + /\ applied' = Append(applied, Head(pending)) + /\ pending' = Tail(pending) + /\ UNCHANGED <> + +Next == + \/ \E q \in {"ble", "main"}: Issue(q) + \/ Drain + +Spec == Init /\ [][Next]_vars /\ WF_vars(Drain) + +----------------------------------------------------------------------------- +IsPrefix(s, t) == + /\ Len(s) <= Len(t) + /\ \A i \in 1..Len(s): s[i] = t[i] + +(***************************************************************************) +(* Effects must land in the order the operations were issued. If they do *) +(* not, two callers racing over the same camera can observe each other's *) +(* state in the wrong order even though every individual block is atomic -- *) +(* atomicity of each block does not imply a consistent order between them. *) +(***************************************************************************) +AppliedInIssueOrder == IsPrefix(applied, issued) + +\* Everything issued eventually lands. Stated as "applied catches up with +\* issued infinitely often" rather than "all MaxOps are applied": Issue is not +\* a fair action, so a behaviour that simply never issues anything would +\* otherwise fail this for reasons that say nothing about the queue. +PendingAlwaysDrains == []<>(Len(applied) = Len(issued)) + +=============================================================================