プロセス・スレッド・並行性の不変条件

到達目標

1. プロセスの隔離資源とスレッドの共有資源を、障害伝播と通信経路を含めて図示できる

   • 再現条件、interleaving、不変条件、修正、回帰測定を含む実験記録
   • 隔離と共有の失敗半径を比較する5分説明

2. 100回以上の反復で競合を再現し、失敗時のinterleavingと破られた不変条件を記録できる

   • 再現条件、interleaving、不変条件、修正、回帰測定を含む実験記録
   • 競合、deadlock、可視性の仮説を観測で切り分ける回答

3. 同期方法を適用した後に正しさ、停止性、性能を再測定し、別の共有境界で選択を再比較できる

   • 競合、deadlock、可視性の仮説を観測で切り分ける回答
   • 未知のワーカー処理でプロセス分離とスレッド共有を再評価した設計

能力の進行

1. recognize

   アドレス空間、ファイル記述子、実行状態、共有データを隔離または共有の観点で分類できる

   証拠: 再現条件、interleaving、不変条件、修正、回帰測定を含む実験記録

2. explain

   操作のatomicity、可視性、順序性、deadlockを別の正しさ条件として説明できる

   証拠: 隔離と共有の失敗半径を比較する5分説明

3. apply

   失敗頻度を測れる競合実験を作り、明示した不変条件に対して同期方法を適用できる

   証拠: 再現条件、interleaving、不変条件、修正、回帰測定を含む実験記録

4. diagnose

   イベント列、ロック取得順、進捗カウンタからdata race、deadlock、starvationを切り分けられる

   証拠: 競合、deadlock、可視性の仮説を観測で切り分ける回答

5. lead

   信頼境界、障害半径、通信量、デバッグ容易性から隔離単位のレビューを主導できる

   証拠: 未知のワーカー処理でプロセス分離とスレッド共有を再評価した設計

なぜ重要か

並行処理では、同じコードが正しい順序で動くという暗黙の期待が壊れる。二つのworkerが在庫を一つずつ減らすだけでも、読取りと書込みが分離していれば更新を失う。低頻度の競合を「再現しないから直った」と扱うと、負荷が高い本番で不変条件を破る。

プロセスは独立したアドレス空間を持つ実行環境、スレッドはプロセス内の資源を共有する実行単位である。ただし、常にプロセスが重くスレッドが軽いという一軸では選べない。生成方式、OS、通信量、権限境界、クラッシュ時の巻込みが判断を変える。

メンタルモデル

並行性の正しさを四つに分ける。atomicityは操作が途中状態を見せないこと、可視性は一方の書込みを他方が観測できること、順序性は必要な前後関係が成立すること、停止性は処理がいつか進むことである。一つを満たしても他を自動では満たさない。Java SE 21では、あるvolatile書込みは同じfieldへの後続volatile読取りにhappens-beforeするが、stock--全体はread、compute、writeの複合操作である。

「data raceがない」と「業務上のrace conditionがない」も別である。個々のアクセスがatomicでも、在庫確認と確定の間に別操作が入れば業務不変条件を破り得る。守る範囲はコード行ではなく状態遷移で決める。

動く例で考える

lost updateをイベント列で再現する

次をRaceLab.javaとして保存する。racyとsynchronizedは同じJava 21、初期値、worker数、反復数、出力契約を使う。

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.nio.charset.StandardCharsets;
import java.nio.file.Path;
import java.util.Arrays;
import java.util.HashMap;
import java.util.Locale;
import java.util.Map;
import java.util.concurrent.CyclicBarrier;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.concurrent.atomic.AtomicReference;

public final class RaceLab {
    private static final int INITIAL = 1000;
    private static final int PER_WORKER = 500;
    private static final int TRIALS = 200;
    private static final long TIMEOUT_MILLIS = 2000;
    private static final long FAILURE_TIMEOUT_MILLIS = 100;
    private static final Object LOCK = new Object();
    private static volatile int stock;

    private record Trial(
            int finalStock,
            int minimumStock,
            long elapsedNs,
            boolean stalled) {}

    private record OwnerResult(
            int finalStock,
            int minimumStock,
            int dedupePrevented,
            int childExit,
            long startupNs,
            long ipcNs,
            long bytesSent,
            long bytesReceived) {}

    private record FailureProbe(
            boolean timedOut,
            boolean forcedCleanup,
            int childExit) {}

    private static Trial runTrial(String mode) throws InterruptedException {
        stock = INITIAL;
        AtomicInteger minimumStock = new AtomicInteger(INITIAL);
        long start = System.nanoTime();
        if (mode.equals("serial")) {
            stock -= PER_WORKER;
            minimumStock.accumulateAndGet(stock, Math::min);
            stock -= PER_WORKER;
            minimumStock.accumulateAndGet(stock, Math::min);
            return new Trial(
                    stock,
                    minimumStock.get(),
                    System.nanoTime() - start,
                    false);
        }

        CyclicBarrier readsCompleted = new CyclicBarrier(2);
        AtomicReference<Throwable> failure = new AtomicReference<>();
        Runnable operation = mode.equals("racy")
                ? () -> {
                    try {
                        int observed = stock;
                        readsCompleted.await();
                        stock = observed - PER_WORKER;
                        minimumStock.accumulateAndGet(stock, Math::min);
                    } catch (Throwable error) {
                        failure.compareAndSet(null, error);
                    }
                }
                : () -> {
                    synchronized (LOCK) {
                        int observed = stock;
                        stock = observed - PER_WORKER;
                        minimumStock.accumulateAndGet(stock, Math::min);
                    }
                };
        Thread first = new Thread(operation, "worker-A");
        Thread second = new Thread(operation, "worker-B");
        first.start();
        second.start();
        first.join(TIMEOUT_MILLIS);
        second.join(TIMEOUT_MILLIS);
        boolean stalled = first.isAlive() || second.isAlive();
        if (stalled) {
            first.interrupt();
            second.interrupt();
            first.join(TIMEOUT_MILLIS);
            second.join(TIMEOUT_MILLIS);
        }
        if (failure.get() != null) {
            throw new IllegalStateException("worker failed", failure.get());
        }
        return new Trial(
                stock,
                minimumStock.get(),
                System.nanoTime() - start,
                stalled);
    }

    private static long median(long[] sorted) {
        int middle = sorted.length / 2;
        return sorted.length % 2 == 1
                ? sorted[middle]
                : sorted[middle - 1] / 2 + sorted[middle] / 2
                + (sorted[middle - 1] % 2 + sorted[middle] % 2) / 2;
    }

    private static void runThreadTrials(String mode)
            throws InterruptedException {
        int violations = 0;
        int minimumStock = Integer.MAX_VALUE;
        int finalStock = Integer.MIN_VALUE;
        int stalled = 0;
        long[] elapsedNsSamples = new long[TRIALS];
        for (int trial = 0; trial < TRIALS; trial++) {
            Trial result = runTrial(mode);
            finalStock = result.finalStock();
            if (finalStock != 0) {
                violations++;
            }
            minimumStock = Math.min(
                    minimumStock,
                    result.minimumStock());
            if (result.minimumStock() < 0) {
                throw new AssertionError(
                        "negative intermediate stock in " + mode);
            }
            elapsedNsSamples[trial] = result.elapsedNs();
            if (result.stalled()) {
                stalled++;
            }
        }
        long[] sortedElapsed = elapsedNsSamples.clone();
        Arrays.sort(sortedElapsed);
        long totalElapsedNs = Arrays.stream(elapsedNsSamples).sum();
        long elapsedNsMedian = median(sortedElapsed);
        long elapsedNsMin = sortedElapsed[0];
        long elapsedNsMax = sortedElapsed[sortedElapsed.length - 1];

        int expectedViolations = mode.equals("racy") ? TRIALS : 0;
        if (violations != expectedViolations || stalled != 0) {
            throw new AssertionError("unexpected trial result");
        }
        System.out.printf(
                "mode=%s trials=%d expected=%d final=%d min=%d violations=%d stalled=%d elapsed_ns=%d%n",
                mode, TRIALS, 0, finalStock, minimumStock,
                violations, stalled, totalElapsedNs);
        if (mode.equals("racy")) {
            System.out.println(
                    "event=A:read(1000),B:read(1000),A:write(500),B:write(500)");
        }
        System.out.printf(
                Locale.ROOT,
                "{\"schema\":\"race-lab-v3\",\"mode\":\"%s\","
                + "\"trials\":%d,\"expected_final\":0,"
                + "\"final_stock\":%d,\"minimum_stock\":%d,"
                + "\"violations\":%d,\"stalled\":%d,"
                + "\"elapsed_ns_median\":%d,"
                + "\"elapsed_ns\":{\"samples\":%s,\"min\":%d,"
                + "\"median\":%d,\"max\":%d,\"total\":%d}}%n",
                mode,
                TRIALS,
                finalStock,
                minimumStock,
                violations,
                stalled,
                elapsedNsMedian,
                Arrays.toString(elapsedNsSamples),
                elapsedNsMin,
                elapsedNsMedian,
                elapsedNsMax,
                totalElapsedNs);
    }

    private static void runOwner() throws Exception {
        int ownerStock = INITIAL;
        Map<String, int[]> applied = new HashMap<>();
        BufferedReader input = new BufferedReader(
                new InputStreamReader(
                        System.in,
                        StandardCharsets.US_ASCII));
        PrintWriter output = new PrintWriter(
                new OutputStreamWriter(
                        System.out,
                        StandardCharsets.US_ASCII),
                true);
        output.println("READY");
        String line;
        while ((line = input.readLine()) != null) {
            if (line.equals("GET")) {
                output.printf("STATE,%d%n", ownerStock);
                continue;
            }
            if (line.equals("STOP")) {
                output.printf("STOPPED,%d%n", ownerStock);
                return;
            }
            String[] fields = line.split(",", -1);
            if (fields.length != 2
                    || !fields[0].matches(
                            "[A-Za-z0-9][A-Za-z0-9._-]{0,63}")
                    || !fields[1].matches("[0-9]+")) {
                throw new IllegalArgumentException("invalid owner request");
            }
            int decrement = Integer.parseInt(fields[1]);
            if (decrement < 0 || decrement > INITIAL) {
                throw new IllegalArgumentException("invalid decrement");
            }
            int[] previous = applied.get(fields[0]);
            if (previous != null) {
                if (previous[0] != decrement) {
                    throw new IllegalArgumentException(
                            "request ID reused with another decrement");
                }
                output.printf(
                        "RESULT,%s,%d,true%n",
                        fields[0],
                        previous[1]);
                continue;
            }
            if (ownerStock - decrement < 0) {
                throw new IllegalStateException("negative stock");
            }
            ownerStock -= decrement;
            applied.put(
                    fields[0],
                    new int[] {decrement, ownerStock});
            output.printf(
                    "RESULT,%s,%d,false%n",
                    fields[0],
                    ownerStock);
        }
        throw new IllegalStateException("owner input ended before STOP");
    }

    private static void runStalledOwner() throws InterruptedException {
        System.out.println("READY");
        System.out.flush();
        while (true) {
            Thread.sleep(TIMEOUT_MILLIS);
        }
    }

    private static ProcessBuilder ownerProcess(String mode) {
        String javaBinary = Path.of(
                System.getProperty("java.home"),
                "bin",
                "java").toString();
        return new ProcessBuilder(
                javaBinary,
                "-cp",
                System.getProperty("java.class.path"),
                RaceLab.class.getName(),
                mode);
    }

    private static String readLineWithTimeout(
            BufferedReader reader,
            ExecutorService readerExecutor) throws Exception {
        Future<String> future = readerExecutor.submit(reader::readLine);
        try {
            String line = future.get(
                    TIMEOUT_MILLIS,
                    TimeUnit.MILLISECONDS);
            if (line == null) {
                throw new IllegalStateException("owner output ended");
            }
            return line;
        } catch (TimeoutException error) {
            future.cancel(true);
            throw new IllegalStateException("owner response timeout", error);
        }
    }

    private static String exchange(
            BufferedWriter input,
            BufferedReader output,
            ExecutorService readerExecutor,
            String request) throws Exception {
        input.write(request);
        input.newLine();
        input.flush();
        return readLineWithTimeout(output, readerExecutor);
    }

    private static OwnerResult exerciseOwner() throws Exception {
        Process child = null;
        ExecutorService readerExecutor =
                Executors.newSingleThreadExecutor();
        long startupStart = System.nanoTime();
        try {
            child = ownerProcess("owner").start();
            BufferedWriter input = new BufferedWriter(
                    new OutputStreamWriter(
                            child.getOutputStream(),
                            StandardCharsets.US_ASCII));
            BufferedReader output = new BufferedReader(
                    new InputStreamReader(
                            child.getInputStream(),
                            StandardCharsets.US_ASCII));
            String ready = readLineWithTimeout(output, readerExecutor);
            long startupNs = System.nanoTime() - startupStart;
            if (!ready.equals("READY")) {
                throw new IllegalStateException("owner did not become ready");
            }

            String[] requests = {"A,500", "A,500", "B,500", "GET", "STOP"};
            String[] expected = {
                "RESULT,A,500,false",
                "RESULT,A,500,true",
                "RESULT,B,0,false",
                "STATE,0",
                "STOPPED,0",
            };
            long bytesSent = 0;
            long bytesReceived = ready.getBytes(
                    StandardCharsets.US_ASCII).length + 1;
            int minimumStock = INITIAL;
            int dedupePrevented = 0;
            long ipcStart = System.nanoTime();
            for (int index = 0; index < requests.length; index++) {
                String response = exchange(
                        input,
                        output,
                        readerExecutor,
                        requests[index]);
                if (!response.equals(expected[index])) {
                    throw new IllegalStateException(
                            "unexpected owner response: " + response);
                }
                bytesSent += requests[index].getBytes(
                        StandardCharsets.US_ASCII).length + 1;
                bytesReceived += response.getBytes(
                        StandardCharsets.US_ASCII).length + 1;
                if (response.endsWith(",true")) {
                    dedupePrevented++;
                }
                String[] fields = response.split(",");
                if (fields.length >= 2
                        && fields[fields.length - 1].matches("[0-9]+")) {
                    minimumStock = Math.min(
                            minimumStock,
                            Integer.parseInt(fields[fields.length - 1]));
                } else if (fields.length >= 3
                        && fields[fields.length - 2].matches("[0-9]+")) {
                    minimumStock = Math.min(
                            minimumStock,
                            Integer.parseInt(fields[fields.length - 2]));
                }
            }
            long ipcNs = System.nanoTime() - ipcStart;
            if (!child.waitFor(TIMEOUT_MILLIS, TimeUnit.MILLISECONDS)) {
                throw new IllegalStateException("owner exit timeout");
            }
            int childExit = child.exitValue();
            if (childExit != 0) {
                throw new IllegalStateException(
                        "owner exited " + childExit);
            }
            return new OwnerResult(
                    0,
                    minimumStock,
                    dedupePrevented,
                    childExit,
                    startupNs,
                    ipcNs,
                    bytesSent,
                    bytesReceived);
        } finally {
            if (child != null && child.isAlive()) {
                child.destroyForcibly();
                if (!child.waitFor(
                        TIMEOUT_MILLIS,
                        TimeUnit.MILLISECONDS)) {
                    throw new IllegalStateException(
                            "owner force cleanup failed");
                }
            }
            readerExecutor.shutdownNow();
            if (!readerExecutor.awaitTermination(
                    TIMEOUT_MILLIS,
                    TimeUnit.MILLISECONDS)) {
                throw new IllegalStateException(
                        "owner reader cleanup failed");
            }
        }
    }

    private static FailureProbe exerciseFailureRadius()
            throws Exception {
        Process child = null;
        BufferedReader output = null;
        ExecutorService readerExecutor =
                Executors.newSingleThreadExecutor();
        try {
            child = ownerProcess("owner-stall").start();
            output = new BufferedReader(
                    new InputStreamReader(
                            child.getInputStream(),
                            StandardCharsets.US_ASCII));
            if (!readLineWithTimeout(output, readerExecutor).equals("READY")) {
                throw new IllegalStateException(
                        "stalled owner did not become ready");
            }
            boolean timedOut = !child.waitFor(
                    FAILURE_TIMEOUT_MILLIS,
                    TimeUnit.MILLISECONDS);
            boolean forcedCleanup = false;
            if (timedOut) {
                forcedCleanup = true;
                child.destroyForcibly();
            }
            if (!child.waitFor(TIMEOUT_MILLIS, TimeUnit.MILLISECONDS)) {
                throw new IllegalStateException(
                        "stalled owner force cleanup failed");
            }
            return new FailureProbe(
                    timedOut,
                    forcedCleanup,
                    child.exitValue());
        } finally {
            if (output != null) {
                output.close();
            }
            if (child != null && child.isAlive()) {
                child.destroyForcibly();
                child.waitFor(TIMEOUT_MILLIS, TimeUnit.MILLISECONDS);
            }
            readerExecutor.shutdownNow();
            if (!readerExecutor.awaitTermination(
                    TIMEOUT_MILLIS,
                    TimeUnit.MILLISECONDS)) {
                throw new IllegalStateException(
                        "stalled owner reader cleanup failed");
            }
        }
    }

    private static void runProcessMessage() throws Exception {
        OwnerResult owner = exerciseOwner();
        FailureProbe failure = exerciseFailureRadius();
        if (owner.minimumStock() < 0
                || owner.finalStock() != 0
                || owner.dedupePrevented() != 1
                || !failure.timedOut()
                || !failure.forcedCleanup()) {
            throw new AssertionError("unexpected process-message result");
        }
        long elapsedNs = owner.startupNs() + owner.ipcNs();
        System.out.printf(
                "mode=process-message trials=1 expected=%d final=%d min=%d violations=%d stalled=%d elapsed_ns=%d%n",
                0,
                owner.finalStock(),
                owner.minimumStock(),
                0,
                0,
                elapsedNs);
        System.out.printf(
                Locale.ROOT,
                "{\"schema\":\"race-lab-v3\","
                + "\"mode\":\"process-message\","
                + "\"trial_scope\":"
                + "\"single-owner-session-not-200-thread-trials\","
                + "\"protocol\":[\"A,500\",\"A,500\","
                + "\"B,500\",\"GET\",\"STOP\"],"
                + "\"final_stock\":%d,\"minimum_stock\":%d,"
                + "\"dedupe_prevented\":%d,\"child_exit\":%d,"
                + "\"startup_ns\":%d,\"ipc_ns\":%d,"
                + "\"bytes_sent\":%d,\"bytes_received\":%d,"
                + "\"failure_probe_timed_out\":%b,"
                + "\"forced_cleanup\":%b,"
                + "\"failure_probe_exit\":%d,"
                + "\"parent_continued\":true,"
                + "\"failure_radius\":\"owner-child-process\"}%n",
                owner.finalStock(),
                owner.minimumStock(),
                owner.dedupePrevented(),
                owner.childExit(),
                owner.startupNs(),
                owner.ipcNs(),
                owner.bytesSent(),
                owner.bytesReceived(),
                failure.timedOut(),
                failure.forcedCleanup(),
                failure.childExit());
    }

    public static void main(String[] args) throws Exception {
        if (args.length != 1) {
            throw new IllegalArgumentException(
                    "usage: java RaceLab "
                    + "racy|synchronized|serial|process-message");
        }
        if (args[0].equals("owner")) {
            runOwner();
        } else if (args[0].equals("owner-stall")) {
            runStalledOwner();
        } else if (args[0].equals("process-message")) {
            runProcessMessage();
        } else if (args[0].equals("racy")
                || args[0].equals("synchronized")
                || args[0].equals("serial")) {
            runThreadTrials(args[0]);
        } else {
            throw new IllegalArgumentException(
                    "usage: java RaceLab "
                    + "racy|synchronized|serial|process-message");
        }
    }
}

java --version
javac RaceLab.java
java RaceLab racy | tee race-before.txt
java RaceLab synchronized | tee race-after.txt
java RaceLab serial | tee serial.txt
java RaceLab process-message | tee process-message.txt
/usr/bin/time -p java RaceLab synchronized
/usr/bin/time -p java RaceLab serial
/usr/bin/time -p java RaceLab process-message

thread三方式の出力契約はmode=... trials=200 expected=0 final=... min=... violations=... stalled=... elapsed_ns=...と、その直後のJSONである。JSONは全200件のelapsed_ns.samples、min、median、max、totalを保持する。各TrialのminimumStockは書込み直後に更新するため最終値の別名ではなく、racy、synchronized、serialの全方式で試行中の負数がないことをassertする。racy版はCyclicBarrierで両workerのreadを先に完了させるため、schedulerやyieldの偶然ではなく全200試行で最小lost updateを構成する。synchronized版とserial版は同じ1000件相当の固定fixtureで200試行0違反を要求し、join timeoutとisAliveで停止性を検査する。なお、一般の確率的raceでは一回の非再現を修正証拠にしない。

前提

Java 21、在庫1000、worker AとBが各500件分を減らす。不変条件はexpected final 0、負数なし、stalled 0。

入力

同じ1000件の減算fixtureをracy、synchronized、serialへ渡し、各200試行する。

操作

racy版では両read後にbarrierを解放して二つのwriteを行い、同期版ではread-subtract-write全体を同じmonitorで囲む。

観測

最小event列はA:read(1000)、B:read(1000)、A:write(500)、B:write(500)で、expected 0に対しfinal 500となる。thread三方式ではfinal、試行中minimum、violations、stalled、200個のelapsed分布を比較する。

結論

synchronizedでread-modify-write全体を囲む。修正後200試行0違反と、monitor unlockから後続lockへのhappens-beforeを組にして修正根拠にする。

性能値はSystem.nanoTimeと/usr/bin/time -pの実測だけを報告し、例示値を捏造しない。process-messageは共有memory版の200試行へ混ぜず、single-owner-session-not-200-thread-trialsという別の測定単位にする。RaceLab自身がowner子プロセスを起動し、標準入力protocolをrequestId,decrement、GET、STOPに固定する。A,500、同じA,500、B,500、GET、STOPを送り、重複Aを二重減算しないこと、final/minimum 0、送受信byte、正常child exit、process起動時間とIPC時間を機械可読JSONへ分離して記録する。さらに別の停止用childを100msでtimeoutさせ、destroyForcibly、exit確認後も親が結果を出せた事実を、共有heapを巻き込まない障害半径の実測証拠にする。

ラボ成果物: 「競合を再現し不変条件で修正した実験記録」には、失敗頻度、最小interleaving、同期前後のコード差、停止性、性能分布を含める。

トレードオフと失敗モード

もっともらしい誤診と反証

1. 誤診: 「二workerが止まったのでdeadlock」。反証: lock取得と待機の循環を記録する。I/O待ちなら外部完了で進み、starvationなら他workerだけ進捗する。停止だけでは循環待ちを証明しない。
2. 誤診: 「Java volatileを付けて100回通ったのでrace修正済み」。反証: read-modify-writeをeventへ分解し、同じinterleavingがJava Language Specification上可能か確認する。volatileがvisibilityとorderingのhappens-beforeを作っても複合incrementのatomicityを保証しない。

lock範囲を広げると不変条件は守りやすいが並列性が下がり、複数lockは並列性を上げる一方で順序規約が必要になる。timeoutでlockを諦める場合も、途中状態のrollbackまたは再試行契約が要る。

知識チェック

1. 整数代入がatomicならcounter増加もatomicか。通常は同じではない。増加はread、compute、writeの複合操作になり得る。
2. process間ならraceは起きないか。共有memory、file、databaseを介せば起きる。address space隔離は全資源の隔離ではない。
3. lockを一つにすればdeadlockは消えるか。そのlock同士の循環は避けやすいが、callback、I/O、再入、別資源待ちを含む停止性は別に確認する。

5分teach-back

lost updateの四イベントを描き、不変条件、atomicity、可視性、停止性を区別する。mutex案とmessage passing案の障害半径を一つずつ述べる。

未知へのtransfer

プロセス分離とスレッド共有の再比較を、画像変換pluginまたは機密データ集計へ適用する。CPU時間だけでなく、権限、入力の信頼度、IPC量、worker crash後の再実行を評価し直す。

出典と次の学習

Java Language Specification SE 21 Chapter 17はthread、monitor、volatile、happens-beforeの正準、POSIX.1-2024のpthread_createとforkは生成後に共有または複製される実行文脈、Linux kernel memory barriers文書はkernel実装上の順序保証、MicrosoftのProcesses and ThreadsはWindows上の資源境界を確認するために使う。異なる言語・OSの契約を混ぜず、正確なURLはmetadataのsourcesに置いた。

次はネットワークの部分失敗を扱い、process外の待機と期限を時系列で診断する。1日後はinterleaving、7日後はdeadlock反証、30日後は実コードの不変条件、90日後は隔離単位の判断を再レビューする。

実践ラボ

在庫更新のlost updateを再現して不変条件で直す

提出成果物: 競合を再現し不変条件で修正した実験記録

1. Java 21で教材のRaceLab.javaをコンパイルし、volatile intへの非atomicなread-modify-writeを200試行する
2. 最終値は0であり負数にならないという不変条件を先に明文化し、違反回数を記録する
3. 失敗試行の読取り、計算、書込みinterleavingを最小のイベント列として再構成する
4. Java synchronizedでread-modify-write全体を修正し、同じ200試行で不変条件と停止性を確認する
5. 直列、同期ありスレッド、プロセス間メッセージの所要時間と障害半径を比較する

説明して理解を確かめる

5分で、プロセスとスレッドの共有境界、lost updateのinterleaving、Java volatileがvisibilityとorderingを扱っても複合incrementのatomicityを得られない理由を説明する。

アセスメント

1. 問い: 二つのworkerが停止した。『deadlockだ』という診断を確定するために必要な証拠と、別のもっともらしい原因を示す。

   期待する証拠: 待機資源とロック取得順の循環、進捗観測、I/O待ちまたはstarvationとの反証

2. 問い: 共有変数へvolatileを付けたら再現しなくなった。修正完了と判断できない理由は何か。

   期待する証拠: Java SE 21のvolatile happens-before、複合操作のatomicity、確率的な一回の非再現を分けた説明

別問題へ転用する

プロセス分離とスレッド共有の再比較

復習スケジュール

1. 1日後

   atomicity、可視性、順序性のうち、今回の不変条件に必要なのはどれか

2. 7日後

   deadlock説を反証する最小のイベント証拠は何か

3. 30日後

   隔離を強めると通信と復旧の設計はどう変わるか

4. 90日後

   atomicity、可視性、順序性のうち、今回の不変条件に必要なのはどれか

評価ルーブリック

出典

以下の外部資料は利用者が選択したときだけ開きます。

• Chapter 17. Threads and Locks (standard)
• pthread_create — thread creation (standard)
• fork — create a new process (standard)
• Linux kernel memory barriers (primary)
• About Processes and Threads (primary)