From 2e0432327fbf6a5eb7ce46b90079e0e618b4deb4 Mon Sep 17 00:00:00 2001 From: Kevin Blackburn-Matzen Date: Sat, 18 Jul 2026 20:44:30 -0700 Subject: [PATCH] Run connection state as atomic blocks on one queue, and serialise reassembly MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit BLEManager keeps connection state in three @Published dictionaries that are read from the CoreBluetooth delegate queue and mutated on main. Swift Dictionary is not thread-safe, so concurrent access is undefined behaviour rather than a stale read, 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. That is the shape several sites already had, and it leaves the read racing and the decision stale. What is required is that the whole read-decide-write runs as one block on a single queue. Main is that queue for connection state, since these properties drive SwiftUI and must be published on main regardless. Sites corrected, all of which split the read from the write across a queue hop: handleConnectionSuccess looked up connectingGoPros on the CoreBluetooth queue and inserted that reference into connectedGoPros in a later main block, so the camera could be removed in between and the stale reference reinserted. didDiscover checked "already connected?" on the CoreBluetooth queue and acted on the answer in a dispatched block. powerDownGoPro looked up the camera on the caller's queue and dispatched only the removal. setDateTime, the WiFi response callbacks, and the device-query timer all read state off the state queue. Two reads were simply unnecessary and are gone: handleCommandResponse looked up a camera for a display name already in scope, and createAppStateContext built crash-report context from the CoreBluetooth queue. onStateQueue always dispatches rather than running inline when already on main. Running inline is faster but makes the order blocks land in depend on which thread issued them — work dispatched earlier from the CoreBluetooth queue would still be waiting while a later main-thread caller ran immediately. Atomicity of each block does not by itself give a consistent order between blocks. assertOnStateQueue traps in debug builds when connection state is touched off the state queue, so a new call site fails immediately in development rather than corrupting memory occasionally in the field. BLEPacketReconstructor had the same hazard on different queues: processPacket runs on the CoreBluetooth queue while checkTimeouts runs on the device-query timer's queue. Its state does not drive SwiftUI, so it gets a dedicated serial queue rather than main, which keeps packet handling off the main thread. specs/ contains the TLA+ models these designs were checked against, with a README describing what each one rules out. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AqfipPBp3eErDgZboooqxP --- Facett/BLEConnectionHandler.swift | 23 ++- Facett/BLEManager+StateQueue.swift | 43 +++++ Facett/BLEManager.swift | 199 ++++++++++++++++------- Facett/BLEPacketReconstructor.swift | 10 +- specs/.gitignore | 2 + specs/BLEConnection.tla | 235 ++++++++++++++++++++++++++++ specs/BLEConnectionFixed.tla | 179 +++++++++++++++++++++ specs/ConnectionConcurrency.tla | 190 ++++++++++++++++++++++ specs/MC_BoundedRetries.cfg | 8 + specs/MC_Conc3.cfg | 8 + specs/MC_ConcLU_current.cfg | 6 + specs/MC_ConcLU_mainAtomic.cfg | 6 + specs/MC_ConcLU_serialQueue.cfg | 6 + specs/MC_ConcLU_writesOnMain.cfg | 6 + specs/MC_Conc_current.cfg | 8 + specs/MC_Conc_mainAtomic.cfg | 8 + specs/MC_Conc_serialQueue.cfg | 8 + specs/MC_Conc_writesOnMain.cfg | 8 + specs/MC_CorrectAttribution.cfg | 9 ++ specs/MC_Fixed.cfg | 10 ++ specs/MC_FixedLiveness.cfg | 8 + specs/MC_FragmentIntegrity.cfg | 9 ++ specs/MC_Liveness.cfg | 8 + specs/MC_MutualExclusion.cfg | 8 + specs/MC_NoOrphanedRetryState.cfg | 8 + specs/MC_NoPartialDelivery.cfg | 9 ++ specs/MC_Order_alwaysAsync.cfg | 7 + specs/MC_Order_inline.cfg | 7 + specs/MC_ReassemblyFixed.cfg | 13 ++ specs/MC_SleepVisibility.cfg | 4 + specs/MC_Sleep_confirmed.cfg | 5 + specs/MC_Sleep_graced.cfg | 5 + specs/MC_Sleep_naive.cfg | 5 + specs/MC_Sleep_original.cfg | 5 + specs/PacketReassembly.tla | 183 ++++++++++++++++++++++ specs/PacketReassemblyFixed.tla | 192 +++++++++++++++++++++++ specs/README.md | 234 +++++++++++++++++++++++++++ specs/SleepState.tla | 199 +++++++++++++++++++++++ specs/SleepVisibility.tla | 172 ++++++++++++++++++++ specs/StateQueueOrdering.tla | 100 ++++++++++++ 40 files changed, 2080 insertions(+), 73 deletions(-) create mode 100644 Facett/BLEManager+StateQueue.swift create mode 100644 specs/.gitignore create mode 100644 specs/BLEConnection.tla create mode 100644 specs/BLEConnectionFixed.tla create mode 100644 specs/ConnectionConcurrency.tla create mode 100644 specs/MC_BoundedRetries.cfg create mode 100644 specs/MC_Conc3.cfg create mode 100644 specs/MC_ConcLU_current.cfg create mode 100644 specs/MC_ConcLU_mainAtomic.cfg create mode 100644 specs/MC_ConcLU_serialQueue.cfg create mode 100644 specs/MC_ConcLU_writesOnMain.cfg create mode 100644 specs/MC_Conc_current.cfg create mode 100644 specs/MC_Conc_mainAtomic.cfg create mode 100644 specs/MC_Conc_serialQueue.cfg create mode 100644 specs/MC_Conc_writesOnMain.cfg create mode 100644 specs/MC_CorrectAttribution.cfg create mode 100644 specs/MC_Fixed.cfg create mode 100644 specs/MC_FixedLiveness.cfg create mode 100644 specs/MC_FragmentIntegrity.cfg create mode 100644 specs/MC_Liveness.cfg create mode 100644 specs/MC_MutualExclusion.cfg create mode 100644 specs/MC_NoOrphanedRetryState.cfg create mode 100644 specs/MC_NoPartialDelivery.cfg create mode 100644 specs/MC_Order_alwaysAsync.cfg create mode 100644 specs/MC_Order_inline.cfg create mode 100644 specs/MC_ReassemblyFixed.cfg create mode 100644 specs/MC_SleepVisibility.cfg create mode 100644 specs/MC_Sleep_confirmed.cfg create mode 100644 specs/MC_Sleep_graced.cfg create mode 100644 specs/MC_Sleep_naive.cfg create mode 100644 specs/MC_Sleep_original.cfg create mode 100644 specs/PacketReassembly.tla create mode 100644 specs/PacketReassemblyFixed.tla create mode 100644 specs/README.md create mode 100644 specs/SleepState.tla create mode 100644 specs/SleepVisibility.tla create mode 100644 specs/StateQueueOrdering.tla 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)) + +=============================================================================