1、技術(shù)創(chuàng)新，變革未來云平臺(tái)存儲(chǔ)系統(tǒng)構(gòu)建方案目錄一個(gè)云廠商的存儲(chǔ)之路將存儲(chǔ)做正確有多難形式化驗(yàn)證是銀彈嗎混沌工程：我想和云存儲(chǔ)談?wù)劥鎯?chǔ)錯(cuò)誤注入一個(gè)云廠商的存儲(chǔ)之路ZStack 是一個(gè)極致產(chǎn)品化、高性能、智能的私有云平臺(tái)在做云平臺(tái)的前幾年，我們一直借助開源存儲(chǔ)：OCFS2、XFS、 NFS因?yàn)樗凶鲞^基礎(chǔ)架構(gòu)的人都會(huì)因存儲(chǔ)詭異的報(bào)錯(cuò)信息、可怕的 調(diào)試難度、驚人的破壞力而敬而遠(yuǎn)之ZStack 的存儲(chǔ)之路20152018 Ceph Community + OCFS2 + Local Storage + 2018 SharedBlock 接管 SAN Storage2019 Mini StorageZSt

2、ack 的存儲(chǔ)之路SharedBlock完整發(fā)揮物理性能極低延遲快速部署對(duì) SAN 廠家、品牌無要求Mini Storage性能近乎完整物理低成本快速部署高穩(wěn)定性將存儲(chǔ)做正確有多難PG 使用 writeback 的機(jī)制，這樣系統(tǒng)可能在后臺(tái)默默 writeback 時(shí)出錯(cuò)此時(shí) IO layer/XFS 會(huì)對(duì)臟頁做 AS_EIO 標(biāo)記，調(diào)用 fsync() 時(shí)返回 EIO但 fsync() 實(shí)際上存在一個(gè)未文檔化的、clear-error-and-continue 的機(jī)制也就是你下一次再調(diào)用 fsync() 時(shí)如果沒有新的標(biāo)記的臟頁，可能就返回成功了！/2019/schedule/event/po

3、stgresql_fsync/PostgreSQL vs fsync()All File Systems Are Not Created Equal上層開發(fā)者往往認(rèn)為崩潰一致性是最基礎(chǔ)的保證實(shí)際上崩潰一致難度也是很高的從文件系統(tǒng)到數(shù)據(jù)庫，已經(jīng)被大家找出無數(shù) Bughttps:/system/files/conference/osdi14/osdi14-paper-pillai.pdf難度一樣不?。号c互聯(lián)網(wǎng)廠商解決的問題不同，但不同廠商的存儲(chǔ)設(shè)備不同廠商的多路徑配置不同的服務(wù)器硬件離散碎片的環(huán)境客戶升級(jí)條件不同有的客戶希望部署完再也不要升級(jí)聯(lián)網(wǎng)條件不同一些客戶機(jī)房連手機(jī)都不允許進(jìn)運(yùn)維水平不同客戶

4、說：我覺得參差不齊的客戶運(yùn)維水平平臺(tái) API、Agent 下命令、DM 設(shè)備操作、分布式鎖、多路徑、SCSI、HBA控制平面和數(shù)據(jù)平面同樣重要甚至控制面具有更可怕的破壞力漫長的路徑形式化驗(yàn)證是銀彈嗎2002 年 Specifying Systems2015 年 How Amazon Web Services Uses Formal Methods2018 年 TLA Workshop被 MongoDB, Elasticsearch 等應(yīng)用TLA+ 的發(fā)展之路State Space Explosion無法轉(zhuǎn)換成代碼，因此在翻譯時(shí)可能出錯(cuò)Spec 的正確性如何驗(yàn)證外部依賴的正確性但涉及算法正確性的

5、證明，形式化證明依然是不可替代的形式化驗(yàn)證所不能解決的問題未來的形式化驗(yàn)證：可視化/will62794/tlaplus_animation未來的形式化驗(yàn)證：易讀http:/tla2018.loria.fr/contrib/liu.pdf未來的形式化驗(yàn)證：可執(zhí)行/UBC-NSS/pgo混沌工程：我想和云存儲(chǔ)談?wù)剢螜C(jī)應(yīng)用向集群應(yīng)用基于系統(tǒng)編程向基于服務(wù)編程對(duì)于基礎(chǔ)設(shè)施軟件可以借鑒嗎？為什么現(xiàn)在都在說混沌工程MTBF長時(shí)間運(yùn)行，隨機(jī)動(dòng)作DPMO反復(fù)迭代測(cè)試Woodpecker數(shù)以萬次的調(diào)用 API不談方法說概念都是耍流氓傳統(tǒng)方法：poweroff tc ifconfig傳統(tǒng)方法的缺點(diǎn)：對(duì)復(fù)雜場(chǎng)景無法模擬 不夠靈活注入什么錯(cuò)誤？云廠商面臨的存儲(chǔ)路徑存儲(chǔ)錯(cuò)誤注入用戶態(tài)錯(cuò)誤注入：libfiu.ar/p/libfiu/內(nèi)核錯(cuò)誤注入：systemtap優(yōu)點(diǎn)相對(duì)靈活 函數(shù)級(jí)別 易于安裝缺點(diǎn)速度慢達(dá)不到 IO 級(jí)別故障塊設(shè)備模擬：device-mapperdm-flakey周期性故障dm-delay 增加延時(shí)故障塊設(shè)備模擬：NBD總結(jié)設(shè)計(jì)階段形式化驗(yàn)證可以減少設(shè)計(jì)的 Bug但并不是銀彈，有成本，有局限開發(fā)階段開發(fā)可測(cè)試代碼注重測(cè)試注重錯(cuò)誤注入總結(jié)手段層面便利程度靈活程度模擬特定模式libfiu用戶態(tài)很方便限制