蔚來Sky天樞操作系統(tǒng)詳解

2024年7月蔚來科技日上，蔚來正式推出Sky.OS即天樞操作系統(tǒng)。

蔚來宣稱這是蔚來歷時(shí)4年研發(fā)、投入超過23,000人/月、面向AI打造的汽車智能底座，對(duì)全生命周期的用戶體驗(yàn)與企業(yè)的體系化效率提升，將發(fā)揮重要作用。

SkyOS·天樞以“1+4+N”的技術(shù)架構(gòu)，實(shí)現(xiàn)這七大特性。

“1”是指多場景優(yōu)化、高性能、高可靠的虛擬機(jī)監(jiān)視器 SkyOS-H，用來管理和調(diào)度整車的異構(gòu)大算力資源，為各個(gè)系統(tǒng)提供安全隔離的運(yùn)行環(huán)境。相比行業(yè)通用方案，SkyOS-H 實(shí)時(shí)任務(wù)時(shí)延縮短 50%，多線程吞吐量提升 40%，虛擬磁盤吞吐提升 15%。

“4”是指SkyOS的4個(gè)操作系統(tǒng)內(nèi)核：

輕量、強(qiáng)可靠性、強(qiáng)實(shí)時(shí)性的 SkyOS-L，支持所有主流車載 MCU 芯片架構(gòu)。相比行業(yè)通用方案，SkyOS-L 實(shí)時(shí)周期性信號(hào)準(zhǔn)時(shí)送達(dá)率提升 30-40%；

基于微內(nèi)核構(gòu)建高安全、強(qiáng)可靠性、強(qiáng)實(shí)時(shí)性的 SkyOS-M，用于中央大腦，主要運(yùn)行車控相關(guān)功能，包括車身、底盤懸架等的高階控制邏輯。SkyOS-M 的核心優(yōu)勢(shì)是安全隔離，在受到同樣影響的情況下，SkyOS-M 的自恢復(fù)速度比 Linux 系統(tǒng)快 100 倍；

面向豐富應(yīng)用場景高性能、實(shí)時(shí)性深度優(yōu)化的 SkyOS-R，部署智能駕駛域的大部分功能。與Linux 發(fā)行版相比，SkyOS-R 在輕負(fù)載情況下實(shí)時(shí)性能高 113 倍，在高負(fù)載情況下實(shí)時(shí)性能高 20 倍，端到端通信延時(shí)小于 1ms，為智駕提供更高的實(shí)時(shí)性性能保障；

面向原生智能深度定制的SkyOS-C，承載絕大多數(shù)的智能座艙功能，實(shí)現(xiàn)低延時(shí)的車云一體化，充分利用云端更大的算力資源與模型，提供更加智能的座艙AI體驗(yàn)。

“N”是指 SkyOS-中間件，是實(shí)現(xiàn)分層解耦、跨域融合的關(guān)鍵，也是支持全生命周期升級(jí)和信息安全保障的基礎(chǔ)。

天樞操作系統(tǒng)是基于德國seL4微內(nèi)核的，2024年10月的seL4峰會(huì)上，蔚來技術(shù)副總裁曲寧做了演講，文檔如下https://sel4.systems/Foundation/Summit/2024/slides/software-defined.pdf。曲寧北大畢業(yè)后去卡梅隆大學(xué)深造，第一份工作是英偉達(dá)系統(tǒng)軟件工程師，然后跳槽到谷歌Linux核心隊(duì)伍，2018年進(jìn)入百度，是百度CarOS首席工程師，阿波羅智能駕駛系統(tǒng)也有參與，2020年進(jìn)入Waymo，負(fù)責(zé)深度學(xué)習(xí)Runtime團(tuán)隊(duì)，2022年進(jìn)入蔚來。

嚴(yán)格講seL4也不是德國的，它是一個(gè)跨國組織，頂級(jí)會(huì)員有四家，分別是地平線、蔚來、悉尼大學(xué)和高頻交易自營商Jump Trading。高級(jí)會(huì)員中知名的只有蘋果，一般會(huì)員基本都是大學(xué)，包括蘇黎世理工學(xué)院、堪薩斯州立大學(xué)、俄勒岡Lewis & Clark大學(xué)、RISC-V國際。此外需要說明，seL4也是Linux基金會(huì)的一員。

微內(nèi)核與宏內(nèi)核區(qū)別

圖片來源：seL4基金會(huì)

微內(nèi)核是將服務(wù)轉(zhuǎn)移到進(jìn)程上的一種內(nèi)核模式。宏內(nèi)核是一種傳統(tǒng)的內(nèi)核結(jié)構(gòu)，它將進(jìn)程管理，內(nèi)存管理等各項(xiàng)服務(wù)功能都放到內(nèi)核中去。微內(nèi)核只保留最低限度的服務(wù)，因此安全性極高，但無法細(xì)粒度運(yùn)行，只能做一個(gè)增強(qiáng)模塊。Linux（安卓）這樣的宏內(nèi)核系統(tǒng)還是不可或缺。這就好比沒有電腦的時(shí)代，一家公司，所有人都在一間辦公室工作，并且每個(gè)人的工作都有關(guān)聯(lián)，都在一個(gè)辦公室，效率自然就很高，但是一個(gè)人感冒了，容易全部都傳染感冒，這就是宏內(nèi)核。微內(nèi)核是一家公司，只保留最低限度的工作人員，只能干部分工作，并且每個(gè)人一間辦公室，大部分工作人員都轉(zhuǎn)移到外地，這樣安全性很高，但效率很低。不過可以提高單個(gè)人的辦公效率就能解決問題。

L4微內(nèi)核家族樹

圖片來源：seL4基金會(huì)

第一代微內(nèi)核是1986年卡內(nèi)基-梅隆大學(xué)的Avie Tevanian和Richard Rashid主導(dǎo)開發(fā)的Mach，第二代即L3和L4，還有至今還很活躍的QNX系統(tǒng)使用的Neutrino內(nèi)核。德國的計(jì)算機(jī)科學(xué)家Jochen Liedtke認(rèn)為Mach的IPC效率低下的原因就是因?yàn)镮PC部分不夠精簡，于是他開發(fā)了L3和L4微內(nèi)核，對(duì)IPC部分進(jìn)行了很徹底的精簡，這項(xiàng)特色保留至今。seL4是在第二代內(nèi)核L4的基礎(chǔ)上發(fā)展而來的，澳大利亞國家信息與通訊技術(shù)部（NICTA）為軍方開發(fā)操作系統(tǒng)時(shí)注意到了完全開源免費(fèi)的L4微內(nèi)核，聯(lián)合新南威爾士大學(xué)對(duì)其進(jìn)行了改造，secure embedded L4誕生，這時(shí)是2009年。seL4不僅繼承了L4內(nèi)核家族的高性能特性，還具備基于端點(diǎn)(endpoint)的IPC機(jī)制。這種IPC機(jī)制最大的特點(diǎn)是使用了能力空間的概念，進(jìn)程在使用IPC請(qǐng)求系統(tǒng)服務(wù)時(shí)必須具備相對(duì)應(yīng)的能力，進(jìn)程持有不可偽造的令牌來表示擁有請(qǐng)求某種服務(wù)的能力。令牌可以被復(fù)制，可以被轉(zhuǎn)移，還可以通過IPC進(jìn)行傳輸。

越大的系統(tǒng)潛在的bug就越多。所以微內(nèi)核在降低bug方面非常有優(yōu)勢(shì)，seL4是世界上最小的內(nèi)核之中的一個(gè)，總共9000行代碼。可是seL4的性能能夠與當(dāng)今性能最好的微內(nèi)核相比。作為微內(nèi)核，seL4為應(yīng)用程序提供少量的服務(wù)，如創(chuàng)建和管理虛擬內(nèi)存地址空間的抽象，線程和進(jìn)程間通信IPC。這么少的服務(wù)靠8700行C代碼完成。seL4是高性能的L4微內(nèi)核家族的新產(chǎn)物，它具有操作系統(tǒng)所必需的服務(wù)，如線程，IPC，虛擬內(nèi)存，中斷等。seL4的實(shí)現(xiàn)被證明是bug-free（沒有bug）的，比如不會(huì)出現(xiàn)緩沖區(qū)溢出，空指針異常等。還有一點(diǎn)就是，C代碼要轉(zhuǎn)換成能直接在硬件上運(yùn)行的二進(jìn)制代碼。seL4能夠確保這個(gè)轉(zhuǎn)換過程不出現(xiàn)錯(cuò)誤，可靠。seL4是世界上第一個(gè)（到目前也是唯一一個(gè)）從很強(qiáng)程度上被證明是安全的OS。

早期高通的手機(jī)使用OKL4 內(nèi)核，出貨量超過10億，而 OKL4 的前身 L4-embed，用在 Apple A7 處理器的一個(gè)安全協(xié)處理器上，地位可能有點(diǎn)像 Intel CPU 里跑的Minix。

SeL4是微內(nèi)核，也是虛擬機(jī)。

SeL4虛擬機(jī)

圖片來源：seL4基金會(huì)

seL4支持用戶模式的VMM，即虛擬機(jī)監(jiān)控，用于虛擬機(jī)時(shí)會(huì)挑系統(tǒng)底層硬件，EL2只用于ARM系統(tǒng)，Root-Ring-0用于x86系統(tǒng)，HS用于RISC-V系統(tǒng)。

來源：蔚來

天樞是全車輛域操作系統(tǒng)，主要是為了適應(yīng)中央計(jì)算系統(tǒng)，需要高可靠性、低延遲和高帶寬，也需要芯片提供完整工具鏈支持，天樞打破了ECU的域邊界，對(duì)供應(yīng)鏈整合也提出了很高的要求。

蔚來數(shù)字架構(gòu)

圖片來源：蔚來

從中不難看出，天樞系統(tǒng)是一個(gè)虛擬機(jī)之上四個(gè)小型操作系統(tǒng)，嚴(yán)格地說與天樞關(guān)聯(lián)最密切的是SkyOS-M，SkyOS-C是一個(gè)改造過的安卓。

來源：蔚來

SkyOS設(shè)計(jì)了多層分級(jí)安全，包括4級(jí)監(jiān)控，3級(jí)恢復(fù)，確保萬無一失，當(dāng)然，這必然消耗CPU算力，需要強(qiáng)大的芯片支撐。

SkyOS-M架構(gòu)

圖片來源：蔚來

上圖看起來非常復(fù)雜，全部使用了專業(yè)的軟件術(shù)語，讓人完全看不懂，要明白這個(gè)圖，需要把“l(fā)ib”即庫，這個(gè)前綴去掉，blk是block，net自然指網(wǎng)絡(luò)，serial自然就是串行，dev就是devices，器件。Srv或sv就是service的縮寫。

底層（MCU抽象層）自然是MCU芯片廠家決定的，seL4處于抽象層之上，virtio 是guest 與host 之間通信的潤滑劑，提供了一套通用框架和標(biāo)準(zhǔn)接口或協(xié)議來完成兩者之間的交互過程，極大地解決了各種驅(qū)動(dòng)程序和不同虛擬化解決方案之間的適配問題。這個(gè)應(yīng)該還是需要底層芯片支持的，圖上也不難看出蔚來的底層MCU是NXP的S32G，存儲(chǔ)系統(tǒng)還是eMMC。LINFLEX是NXP的一個(gè)工具，用來配置UART端口，PL011也是UART關(guān)聯(lián)的。S32GPFE中的PFE即Packet Forwarding Engine ，這是NXP開發(fā)的即以太網(wǎng)加速模塊，模塊支持以太網(wǎng)包的轉(zhuǎn)發(fā)、修改、分類等功能，它基于已在NXP Layerscape系列處理器上驗(yàn)證的解決方案，僅需使用CPU轉(zhuǎn)發(fā)33%的功耗，就可從主機(jī)CPU完全offload網(wǎng)絡(luò)轉(zhuǎn)發(fā)相關(guān)負(fù)載。

sel4之上是process 服務(wù)器，再上是Device服務(wù)器和驅(qū)動(dòng)，再向上是四個(gè)模塊：時(shí)鐘、FS（可能是功能安全）、網(wǎng)絡(luò)和MISC。Libcore貫穿這三層。再向上是musl libc編譯的POSIX系統(tǒng)，是一個(gè)輕量級(jí)的 C 標(biāo)準(zhǔn)庫，它的設(shè)計(jì)目標(biāo)是盡可能小而快，同時(shí)提供最高的代碼質(zhì)量和安全性。musl libc的源代碼通常較短，編譯速度較快，沒有額外的依賴，因此非常適用于嵌入式系統(tǒng)和輕量級(jí)應(yīng)用程序。POSIX是Portable Operating System Interface for Computer Environments 的縮寫，它是ISO C的延伸，POSIX的目的，是統(tǒng)一UNIX-like 的OS對(duì)外的接口，方便OS之上的應(yīng)用在各種OS上移植運(yùn)行，完整的POSIX標(biāo)準(zhǔn)有4000多頁，1000多個(gè)接口。POSIX與AUTOSAR關(guān)系密切，CP中的操作系統(tǒng)部分主要沿用OSEK，而AP的操作系統(tǒng)部分，則明確了是基于POSIX PSE51的。

PSE51并沒有定義進(jìn)程間通訊IPC （inter process communication）， 因此并沒有直接的接口可以實(shí)現(xiàn)進(jìn)程之間的交互。所以進(jìn)程間通信需要有額外模塊支持，例如AUTOSAR AP提供的CM （communication management ）。抽象出來的ARA接口可以用于IPC，統(tǒng)一提供機(jī)器內(nèi)和機(jī)器之間面向服務(wù)的通信。隨著面向服務(wù)架構(gòu)（SOA）在汽車行業(yè)的流行，POSIX提供的標(biāo)準(zhǔn)接口也為以太網(wǎng)通訊和統(tǒng)一服務(wù)接口提供了良好基礎(chǔ)。

POSIX之上是第三方軟件，再向上才是應(yīng)用層。

基于微內(nèi)核的操作系統(tǒng)一般是第三方提供的，蔚來力求垂直集成，也做了。第三方的話，中興通訊也在做，2022年初，中興通訊的汽車操作系統(tǒng)GoldenOS微內(nèi)核產(chǎn)品獲得了SGS頒發(fā)的ISO 26262 ASIL-D級(jí)汽車功能安全產(chǎn)品認(rèn)證證書，中興通訊旗下產(chǎn)品——車用微內(nèi)核操作系統(tǒng)ZTE Automotive OS V3.0正式通過POSIX規(guī)范PSE52實(shí)時(shí)控制器1003.13-2003系統(tǒng)認(rèn)證，成為國內(nèi)首家獲得此認(rèn)證的企業(yè)。當(dāng)然也可以委托第三方，微內(nèi)核也有不少選擇，例如QNX的Neutrino或被Aptiv收購的風(fēng)河（Vxworks混合內(nèi)核），Linux基金會(huì)的微內(nèi)核項(xiàng)目Zephyr。

微內(nèi)核不能取代宏內(nèi)核例如Linux這種大型系統(tǒng)，微內(nèi)核的通訊成本很高，本來傳遞個(gè)地址就可以的事，現(xiàn)在要整個(gè)復(fù)制過去。所以復(fù)雜的功能還是離不開宏內(nèi)核，如同座艙離不開安卓，ADAS也離不開Ubuntu，軟件定義汽車時(shí)代，必然要使用Linux這種大型系統(tǒng)。微內(nèi)核主要用來做做虛擬機(jī)和增強(qiáng)功能安全，當(dāng)然最底層的芯片是最關(guān)鍵的，所以蔚來也做了芯片。

能用比較小眾的seL4微內(nèi)核打造天樞系統(tǒng)，毫無疑問，蔚來的軟件團(tuán)隊(duì)是國內(nèi)所有乃至全球汽車廠家中最強(qiáng)的。