|
| 1 | +// MARK: - Foreign-Region Sending (V5) |
| 2 | +// Purpose: Verify the v1.1.0 concurrency posture of Memory.Foreign — NO Sendable |
| 3 | +// conformance, NO @Sendable finalizer requirement; isolation crossing is |
| 4 | +// region-based sending per [MEM-SEND-010]/[MEM-SEND-012]/[MEM-SEND-013]. |
| 5 | +// Written in the R2 surface (Span.Raw.Mutable + plain closure), under the |
| 6 | +// ecosystem settings loop (.strictMemorySafety() + feature set). |
| 7 | +// Hypothesis: (a) a non-Sendable ~Copyable Foreign whose finalizer captures only |
| 8 | +// Sendable state forms a disconnected region and crosses into another |
| 9 | +// isolation domain as a `sending` argument, where its drop runs the |
| 10 | +// finalizer exactly once; (b) a Foreign whose finalizer captures |
| 11 | +// actor-reachable non-Sendable state is rejected AT THE SEND SITE by the |
| 12 | +// region-isolation checker — per-send checking, no type-level promise. |
| 13 | +// |
| 14 | +// Toolchain: Apple Swift 6.3.2 (swiftlang-6.3.2.1.108 clang-2100.1.1.101) |
| 15 | +// Platform: arm64-apple-macosx26.0 |
| 16 | +// |
| 17 | +// Result: CONFIRMED (both directions) |
| 18 | +// V5a (positive): non-Sendable Foreign (finalizer capturing only Sendable state) |
| 19 | +// crossed into actor isolation as `consuming sending`; finalizer ran exactly |
| 20 | +// once in the sink's isolation. Output: "finalizer exactly-once = 1: CONFIRMED". |
| 21 | +// take() escapes custody without invoking; guarded deinit does not double-run |
| 22 | +// (witness 1 -> 2 only on manual invocation). |
| 23 | +// V5b (-DNEGATIVE_PROBE_SENDING): rejected AT THE SEND SITE — |
| 24 | +// "error: sending 'foreign' risks causing data races [#SendingRisksDataRace]" |
| 25 | +// "note: main actor-isolated 'foreign' is passed as a 'sending' parameter; |
| 26 | +// Uses in callee may race with later main actor-isolated uses" |
| 27 | +// (the finalizer's capture of MainActor-reachable non-Sendable state entangles |
| 28 | +// the value's region; per-send checking, no type-level promise needed). |
| 29 | +// DISCOVERY (surface-shaping): `discard self` requires trivially-destroyed stored |
| 30 | +// properties (Swift 6.3.2) — "can only 'discard' type 'Foreign' if it contains |
| 31 | +// trivially-destroyed stored properties at this time" — so a closure-bearing |
| 32 | +// ~Copyable cannot use the Memory.Contiguous-style discard-based take(); the |
| 33 | +// working shape is the Completion.Entry pattern (Optional field + guarded deinit). |
| 34 | +// ALSO: `sending` alone does not specify ownership for a ~Copyable parameter |
| 35 | +// ("parameter of noncopyable type 'Foreign' must specify ownership"); |
| 36 | +// the spelling is `consuming sending`. |
| 37 | +// Date: 2026-06-12 |
| 38 | +// |
| 39 | +// Hazard notes ([MEM-SEND-009] et al.): no `inout sending` parameters anywhere |
| 40 | +// (merge hazard); no withLock { $0 } capture-return shapes; the exactly-once |
| 41 | +// witness is an Atomic global (referenced, not captured) because a plain class |
| 42 | +// var cannot cross isolation and a captured ~Copyable Mutex would be consumed |
| 43 | +// into the closure. |
| 44 | + |
| 45 | +import Span_Primitives |
| 46 | +import Memory_Primitives |
| 47 | +import Synchronization |
| 48 | + |
| 49 | +// MARK: - The R2 surface (doc v1.1.0 sketch shape) |
| 50 | + |
| 51 | +/// The owning envelope around the ecosystem's existing non-owning descriptor: |
| 52 | +/// `Span.Raw.Mutable` + finalizer + `~Copyable` uniqueness. NOT Sendable — the |
| 53 | +/// closure field opens the region to captures the type cannot see; transferability |
| 54 | +/// is checked per send by region isolation (terminal direction at birth, |
| 55 | +/// [MEM-SEND-013]). |
| 56 | +struct Foreign: ~Copyable { |
| 57 | + let region: Span.Raw.Mutable |
| 58 | + /// Optional SOLELY so `take()` can suppress the deinit's invocation: |
| 59 | + /// `discard self` requires trivially-destroyed stored properties (Swift 6.3.2 |
| 60 | + /// diagnostic, V5 discovery), so a closure-bearing ~Copyable cannot use the |
| 61 | + /// discard-based escape hatch — the working shape is the Completion.Entry |
| 62 | + /// pattern (Optional field + guarded deinit). nil is reachable only via take(). |
| 63 | + var _finalizer: ((Span.Raw.Mutable) -> Void)? |
| 64 | + |
| 65 | + init(adopting region: Span.Raw.Mutable, finalizer: @escaping (Span.Raw.Mutable) -> Void) { |
| 66 | + self.region = region |
| 67 | + self._finalizer = finalizer |
| 68 | + } |
| 69 | + |
| 70 | + consuming func take() -> (region: Span.Raw.Mutable, finalizer: (Span.Raw.Mutable) -> Void) { |
| 71 | + let result = (region, _finalizer!) |
| 72 | + _finalizer = nil |
| 73 | + return result |
| 74 | + } |
| 75 | + |
| 76 | + deinit { |
| 77 | + if let finalizer = _finalizer { finalizer(region) } |
| 78 | + } |
| 79 | +} |
| 80 | + |
| 81 | +extension Foreign: Memory.Region { |
| 82 | + var base: Memory.Address { |
| 83 | + // SAFETY: nonNull guarantees a non-null start even for empty regions. |
| 84 | + unsafe Memory.Address(region.base.nonNull.baseAddress!) |
| 85 | + } |
| 86 | + var capacity: Memory.Address.Count { |
| 87 | + Memory.Address.Count(UInt(unsafe region.base.nonNull.count)) |
| 88 | + } |
| 89 | +} |
| 90 | + |
| 91 | +// MARK: - The other isolation domain |
| 92 | + |
| 93 | +actor Sink { |
| 94 | + /// The Foreign arrives as a `sending` argument and is dropped at the end of |
| 95 | + /// this isolated method — the finalizer runs HERE, not where the value was made. |
| 96 | + func consume(_ foreign: consuming sending Foreign) { |
| 97 | + _ = foreign.capacity |
| 98 | + } |
| 99 | +} |
| 100 | + |
| 101 | +// MARK: - Variant 5a: disconnected-region Foreign crosses as sending (positive) |
| 102 | + |
| 103 | +let v5aFinalized = Atomic<Int>(0) |
| 104 | + |
| 105 | +func variant5a() async { |
| 106 | + let raw = unsafe UnsafeMutableRawBufferPointer.allocate(byteCount: 16, alignment: 16) |
| 107 | + let region: Span.Raw.Mutable = unsafe .init(raw) |
| 108 | + let poolTag = 7 // Sendable capture — the region stays disconnected |
| 109 | + let foreign = Foreign(adopting: region) { r in |
| 110 | + precondition(poolTag == 7) |
| 111 | + unsafe r.base.nullable.deallocate() |
| 112 | + v5aFinalized.wrappingAdd(1, ordering: .relaxed) |
| 113 | + } |
| 114 | + let sink = Sink() |
| 115 | + await sink.consume(foreign) |
| 116 | + let n = v5aFinalized.load(ordering: .sequentiallyConsistent) |
| 117 | + precondition(n == 1, "finalizer must run exactly once, in the sink's isolation") |
| 118 | + print("V5a non-Sendable Foreign sent across isolation, finalizer exactly-once = \(n): CONFIRMED") |
| 119 | + |
| 120 | + // take(): custody escapes WITHOUT invoking; the guarded deinit must not double-run. |
| 121 | + let raw2 = unsafe UnsafeMutableRawBufferPointer.allocate(byteCount: 16, alignment: 16) |
| 122 | + let second = Foreign(adopting: unsafe .init(raw2)) { r in |
| 123 | + unsafe r.base.nullable.deallocate() |
| 124 | + v5aFinalized.wrappingAdd(1, ordering: .relaxed) |
| 125 | + } |
| 126 | + let (takenRegion, takenFinalizer) = second.take() |
| 127 | + precondition(v5aFinalized.load(ordering: .sequentiallyConsistent) == 1, "take() must not invoke") |
| 128 | + takenFinalizer(takenRegion) |
| 129 | + precondition(v5aFinalized.load(ordering: .sequentiallyConsistent) == 2, "manual invocation after take()") |
| 130 | + print("V5a take() escapes custody without invoking; guarded deinit does not double-run: CONFIRMED") |
| 131 | +} |
| 132 | + |
| 133 | +await variant5a() |
| 134 | + |
| 135 | +// MARK: - Variant 5b: actor-entangled Foreign is rejected at the send site |
| 136 | +// (build with -Xswiftc -DNEGATIVE_PROBE_SENDING) |
| 137 | + |
| 138 | +#if NEGATIVE_PROBE_SENDING |
| 139 | +/// Deliberately non-Sendable. |
| 140 | +final class Ledger { |
| 141 | + var entries: [Int] = [] |
| 142 | +} |
| 143 | + |
| 144 | +/// MainActor-reachable state: appending `ledger` here merges it into the |
| 145 | +/// MainActor's region BEFORE the finalizer captures it. (A static, not a |
| 146 | +/// top-level var — top-level code variables cannot carry a global actor.) |
| 147 | +@MainActor |
| 148 | +enum V5B { |
| 149 | + static var retained: [Ledger] = [] |
| 150 | +} |
| 151 | + |
| 152 | +@MainActor |
| 153 | +func variant5b() async { |
| 154 | + let ledger = Ledger() |
| 155 | + V5B.retained.append(ledger) |
| 156 | + let raw = unsafe UnsafeMutableRawBufferPointer.allocate(byteCount: 16, alignment: 16) |
| 157 | + let foreign = Foreign(adopting: unsafe .init(raw)) { r in |
| 158 | + ledger.entries.append(unsafe r.base.nonNull.count) |
| 159 | + unsafe r.base.nullable.deallocate() |
| 160 | + } |
| 161 | + let sink = Sink() |
| 162 | + // EXPECTED: region-isolation diagnostic at this send site — `foreign`'s region |
| 163 | + // includes MainActor-reachable non-Sendable state via the closure capture. |
| 164 | + await sink.consume(foreign) |
| 165 | +} |
| 166 | +#endif |
| 167 | + |
| 168 | +print("done") |
0 commit comments