1、雲端運算與虛擬化 可以說虛擬化是雲端運算的技術基石，同時雲端運算也是虛擬化技術的進一步發展、變革和昇華。 透過對實體設備進行虛擬化，包括運算虛擬化、儲存虛擬化、網路虛擬化等技術，將 IT 基礎資源進行池化，對上層應用屏蔽底層實體設備，進一步提高資源利用率和系統的穩定性。 虛擬化最早的使用場景多為企業內部使用，這也是企業私有雲得以快速推廣實施的重要原因之一。 但相比虛擬化，雲端運算在彈性伸縮、租戶管理、按需調配及編排、自助計費、 IT 營運等方面得到了長足的補充、提高和完善，並且可以支援超大規模的計算和存儲，跨 區域的網路架構等。 雖然雲端運算最早是基於虛擬化這項技術基石，但隨著近幾年的快速發展， 雲端運算已經完美支援ironic 裸設備、 Docker 容器化等技術，並且相互補充、相互完善，共同促進了整個雲 計算生態圈的發展與完善，為不同的應用場景提供不同的最佳技術實務。 2、雲端運算與容器化 容器化是最近幾年呼聲很高、討論很熱的一種技術解決方案，大有取代雲端運算、雲端平台的風頭，網路上也有類似的論調。 對此，我以為容器化應該是雲端運算的組成部分之一，跟虛擬化技術一樣，可以成為雲端運算的技術基石之一，並且二者在某種程度（穩定性、安全性以及主機隔離性 ）上，二者應該是可以互相補充、互相完善的。 容器化比較適合輕應用部署，其對微服務具有天然的支持，透過工具鏈構築DevOps 持續交付平台，可以大大的提高交付效率，特別對於需求多變、迭代頻繁的業務場景，可以極簡地縮短 交貨時間、提高交付效率，同時也可以快速應對訪問量陡增陡減情況下的快速伸縮。 但是，對於傳統的中大型系統（微服務拆分後，比較適合容器化部署，但收益不是很大，因為其係統需求和訪問都相對比較穩定，變化不大）以及數據庫應用不是很適合，就 關係型資料庫不適合容器部署方面，有以下幾點原因： （1） 資料安全方面的問題：由於容器底層技術的限制性和資料庫底層開發相容方面的考慮，容器運行資料庫會存在資料安全的問題，特別是容器異常或是崩潰，資料庫未完全關閉的情況下 ，會損壞資料； （2） 資料庫效能方面的問題：追求關係型資料庫或資料倉儲的高效能時，我們往往會採用裸金屬的方式部署，屏蔽作業系統的一部分瓶頸，或是直接在最佳化之後的OS 上部署，同時 資料庫的效能大多出在IO 方面，採用容器部署運行資料庫，層級複雜、 IO 負載進一步提高，會大大影響資料庫的讀寫效能，與資料庫高效能最佳實務相悖。 （3） 天然的對立面：容器技術特別適合部署運行無狀態的服務，並且其資料持久化依賴於外置設備，而資料庫是典型的有狀態的持久化的服務，二者存在對立的情況，強行 在容器跑資料庫需要考慮狀態持續性以及資料持久化兩大因素。 （4） 資源隔離方面：容器技術在資源隔離方面較虛擬化計畫差不少， Docker 是利用 Cgroup 實現資源限制的，只能限制資源消耗的最大值，而不能隔絕其他程式佔用自己的資源。 如果其他應用程式過渡佔用實體機資源，將會影響容器裡資料庫的讀寫效率。 需要的隔離等級越多，獲得的資源開銷就越多。 鑑於資源隔離的先天不足，在容器整體規劃方面，如果產生統一伺服器上既有應用又有資料庫，那麼在效能方面會相互影響，而在資料庫的最佳實務中，應用程式和資料庫是要分開部署 ，其二者對伺服器資源的需求也是大不一樣的。 但是仍有部分企業將資料庫部署在容器中，特別是 MySQL ，我認為這也是有一定業務場景支持，也是比較合適的。 如：對負責系統進行微服務拆分和資料庫拆分，每個服務對應相應的資料庫，二者綁定較深，這種情況下為了便於管理和擴展，是適合容器部署的，但是在擴展方面 需要結合資料庫的高可用和讀寫分離架構進行；另外還有一種是比較適合運行的，如資料庫本身就是分散式的資料庫且所儲存的資料並不敏感，安全性要求不高，如網站的流量 分析、搜尋的索引詞儲存等，可以利用分佈資料庫的分片來增加實例數，進而增加吞吐量。 3、…

原创 岱军 云云众生s UMass Amherst的Baldur方法能夠自動產生用於驗證程式碼、防範漏洞的證明。 譯自Debugging Software Using Generative AI，作者 Jeffrey Burt 是一位資深記者，擁有三十多年的新聞工作經驗，過去二十多年專注於科技領域。 在過去的16年多里，他曾在eWEEK工作，並在之後成為自由科技記者。 自從OpenAI於2022年11月底推出其ChatGPT聊天機器人以來，生成式人工智慧工具和大型語言模型（LLM）的採用只有加速，深入滲透到各種形狀、大小和行業的組織中，而軟體開發人員並 未對其產生免疫。 生成式人工智慧的用例，如內容創作、對話式人工智慧和語言翻譯，在軟體開發中是多樣化且不斷增長的，涉及程式碼優化和生成、錯誤修復、文件編寫以及持續整合等方面。 根據卡內基美隆大學SEI部落格中的AI專家在2023年10月的一篇文章稱，開發人員越來越認為生成式人工智慧是一個有用的工具。 作者寫道：“關於使用LLM進行軟體開發的最初炒作已經開始冷卻，現在的期望更加現實。”，“對話已經從期望LLM取代軟體開發人員（即人工智慧）轉變為將LLM視為合作夥伴， 並集中在最佳應用它們的地方（即增強型智能）。” LLM和軟體驗證 上個月，由馬薩諸塞大學阿默斯特分校的電腦科學家領導的一組人表示，他們正在利用生成式人工智慧和LLM的力量來解決驗證程式碼的棘手挑戰，以幫助防止軟體中的漏洞。 具體而言，該團隊專注於利用人工智慧開發一種方法，自動產生完整的證明以用於驗證軟體程式碼。 這是一項費時、昂貴且耗時的過程，通常透過手動程序完成。 更困難的過程是機器檢查：創建一個數學證明來展示程式碼是否符合預期，然後使用定理提供者確保證明的正確性。 Emily First在完成她的電腦科學博士學位後成為加州大學聖迭戈分校的博士後研究員，而她在馬薩諸塞大學阿默斯特分校攻讀博士學位期間的研究涉及LLM和軟體驗證，並成為她博士論文的一部分。 她指出，手動編寫證明所需的時間可能比編寫軟體程式碼本身還要多。 因此，根據馬薩諸塞大學阿默斯特分校資訊與電腦科學曼寧學院的教授、本文的高級作者Yuriy Brun的說法，實際上經過正式驗證的系統數量相當有限。 「這很難，」Brun告訴The New Stack。 “這就是我們介入的地方。我們試圖解決的問題是自動產生這些證明。” 不應該接受有錯誤的軟體 這樣做將有助於解決一個更大的問題：軟體中存在缺陷，這可能是煩人的，或者——如果被網路攻擊者利用或存在於可能對廣泛產生負面影響的複雜系統中——是危險 的。 「軟體是我們日常生活中重要的一部分，」布倫說。 「你什麼都做不了。你不能開車，不能坐電梯，都離不開軟體。不幸的是，今天的軟體通常是有漏洞的。我們幾乎期望在商店購買的任何軟體都會有一些錯誤。這只是 一個難以解決的問題，因此有很多不同的方法來嘗試提高軟體的品質。” 其中一個方法是證明軟體是正確的。 這是一種有效的方法，但也是最困難的方法之一。 在某些領域，這已經被實踐，例如在醫療領域用於某些醫療設備或由NASA使用，「因為如果你的太空船上有一個錯誤，你的軟體崩潰了，那將是代價高昂的， 所以實際上有開發人員和軟體工程師正式證明函數的正確性是值得的。」他說。 一些研究人員已經創建了能夠一行一行地寫證明的模型，先寫證明的前10行，然後讓模型基於已經寫的內容以及試圖證明的內容搜索，找出下一行最有可能是什麼。 建構Baldur 馬薩諸塞大學阿默斯特分校的研究人員將目光投向LLM，作為自動產生證明的可能解決方案。 然而，即使這也帶來了挑戰，最大的挑戰之一是這些模型並不總是正確的。 與其崩潰——從而讓開發人員知道有些事情出錯了——它們會“悄悄失敗”，生成一個錯誤的答案但將其呈現為正確的。 悄悄失敗通常是最糟糕的事情，布倫說。 EnterBaldur，這是馬薩諸塞大學阿默斯特分校團隊創建的一種新的基於人工智慧的證明方法。 研究人員使用了Google的Minerva LLM，該模型經過大量自然語言文本的訓練。 然後，它進一步在118GB的數學科學論文和包含數學表達式的網頁上進行訓練，然後在Isabell/HOL上進行了更多的訓練，這是一種用於編寫數學證明的語言。 然後，Baldur產生了整個證明，使用Isabelle，一個定理證明器，對整個世界進行檢查。…