大型語言模型（LLM）驅動的軟體開發中的一個主要趨勢是，可驗證的正確性可以讓我們更容易地在 LLM 上進行更大的飛躍。例如，測試、編譯器、狀態機等。在為 databuild 研究的過程中，我最近接觸到了彩色網狐網路（colored petri nets），並立刻看到了機會。

彩色網狐網路（CPN）是網狐網路的擴展。網狐網路本質上是有向二分圖，其中「地點」（places）可以包含「代幣」（tokens），而地點由「轉換」（transitions，副作用發生的地方）連接。在網狐網路中，單個代幣不包含數據，代表了代幣在網路中沒有身份的位置。重要的是，具有僅有一個輸入和輸出轉換且全局只有一個代幣的網狐網路等同於有限狀態機。彩色網狐網路擴展了這個模型，允許個別代幣附加數據。這使得 CPN 能夠緊密匹配 Rust 的類型狀態模式（Rust typestate pattern），並暗示 Rust 可能能夠輕鬆實現 CPN 的語義。

CPN 之所以特別引人注目，是因為 a) 編寫併發應用程式仍然很困難，b) 它們提供了在建置時形式化驗證併發程式的潛力。此外，如果我們能在底層實現一個高效能的資料儲存，CPN 框架可能能夠處理併發應用程式的難點：狀態同步、衝突檢測、死鎖避免以及協調對共享資源的存取。這些功能透過 CPN 的另外兩個特性實現：守衛（guards）和多代幣消耗/生產（multi-token consumption/production）。

守衛是適用於轉換的一系列布林條件：代幣要進行該轉換必須滿足的條件。例如，要領取一個連線池中的連線，必須有超過 0 個可用連線。多代幣消耗/生產顧名思義：透過轉換在網路中形成分支，例如 P1 -> T1 -> (P2, P3)，因此 T1 從 P1 消耗一個代幣，同時在 P2 和 P3 中產生一個代幣。反之，透過轉換在網路中形成匯合，例如 (P1, P2) -> T1 -> P3，這需要 P1 和 P2 都存在能夠透過 T1 轉換到 P3 的代幣，這也將是同時發生的。

一個涉及輕度併發的應用程式是使用租賃代理和爬取目標的網路爬蟲。您有有限數量的代理可用於代理您的請求，並且需要限制您對所有代理的使用速率，以確保它們不會過度請求給定的目標。此外，您希望避免同時多次請求同一目標，並避免過於頻繁地向某個網域發送請求，以成為一個負責任的使用者。傳統上，這透過中央資料庫的資源租賃來解決，透過資料庫中的 `select for update` 風格語義實現。我們可以想像使用 CPN 語義來實現這一點，將 `scrape_target` 轉換視為 `available_proxies` 和 `prioritized_targets` 地點的匯合，只有在有可用代理和優先目標可用時，爬取才會開始。您也可以想像使用 CPN 語義實現其他複雜的分散式爬蟲功能：

另一個應用程式是 databuild，其中網路由分割區（實際上是租賃給作業執行）、需求和作業執行組成，我們將受益於某種自我組織的動態過程來傳播資料依賴關係，並以安全、高效且快速的方式解決使用者指定的分割區需求。但關於那個傢伙的更多資訊稍後再說。

我還在摸索這個部分，但似乎有幾種合理或有趣的實現 CPN 的策略：

我正在努力解決的一個問題是如何解決分割問題：如果應用程式狀態變得太大而無法容納單一伺服器的記憶體，是否有辦法自動分割網路/代幣以實現無畏的併發和水平擴展性？到目前為止，答案似乎是 a) 在應用程式中解決，將封存地點/轉換作為網路的一部分，或 b) 在資料庫層級解決。或者也許是更瘋狂的東西，整個網路由多個 CPN 應用程式組成，它們本身暴露查詢/消耗介面？

總結來說，如果我們能夠找到一個具有合理持久性的 CPN 應用程式框架，我們就可以對代理編寫的程式碼施加更多的建置時約束（有利於開發速度），同時還能提供開箱即用的正確性保證和模擬功能，這是不受約束的計算應用程式無法提供的。令人興奮！

為了驗證這一點，我們需要一個真實的挑戰：用 CPN 語義重寫某個東西並進行比較。核心問題不是「CPN 能否快速/正確」——當然可以。問題是：這種範式是否能讓編寫簡單、正確且快速的併發程式變得更容易？形式化是否能透過減少錯誤和客製化協調程式碼來證明其價值？

賭注：爬蟲排程器（spider-rs）

使用 CPN 實現爬蟲的決策核心——URL 優先級、網域速率限制、代理分配、重試排程。模擬 HTTP 層；與原始程式碼相比，對決策/秒進行基準測試並比較協調程式碼的複雜性。

為什麼是爬蟲？傳統的實現充滿了臨時的協調：速率限制圖、冷卻追蹤器、重試計數器、網域佇列。這正是 CPN 所形式化的。正確性很重要（禮貌違規會讓你被封鎖），而定時轉換是核心，而不是附帶的。spider-rs 已經是 Rust 了，所以我們可以分叉並直接比較。

記憶體中的 Rust 與 SQLite 快照：單線程，移動語義適用，速度極快。分割 = 獨立的二進位檔案，具有不相交的代幣所有權（可在網路定義時透過分割區金鑰要求強制執行）。模擬 = 相同的 CPN 執行，具有模擬效果，可進行正確性測試、故障注入和時間快轉。