Tiêu chuẩn C++ được dùng trong F-35 - Vì sao máy bay chiến đấu cấm 90% tính năng của C++
(youtube.com)- Video giải thích vì sao phần mềm cho tiêm kích và tên lửa nơi một lỗi chỉ trong một dòng có thể dẫn đến hậu quả chí mạng lại loại bỏ phần lớn tính năng của C++ để chỉ giữ lại phần mã có thể dự đoán được
- Tóm lược lịch sử từ máy tính ném bom cơ khí của F-4, bộ vi xử lý bí mật của F-14, đến cuộc chiến ngôn ngữ quân sự với Jovial·CMS-2·Ada, cùng sự bùng nổ mã nguồn đã dẫn tới nhu cầu về một ngôn ngữ an toàn thống nhất và tiêu chuẩn nghiêm ngặt
- Trình bày bằng mã thực tế cách tiêu chuẩn JSF C++ được Lockheed tạo ra khi thuyết phục sử dụng C++ thay vì Ada trong quá trình phát triển F-35, với việc cấm ngoại lệ, đệ quy, cấp phát bộ nhớ động và thay thế bằng mã trả về, vòng lặp, đặt trước bộ nhớ...
- Cùng với việc máy tính nhiệm vụ đời đầu của F-35 dùng kiến trúc dòng PowerPC, video kết nối X-Plane 12 với một MFD tự chế để so sánh trong lúc bay việc mã vi phạm quy tắc JSF và mã tuân thủ khác nhau ra sao trong thực tế
- Kết luận rằng tiêu chuẩn JSF sau này đã dẫn tới các tiêu chuẩn an toàn như NASA F-Prime·MISRA·AutoSAR, và hiện nay sẽ phù hợp hơn nếu sử dụng C++ Core Guidelines và C++ hiện đại trên nền di sản đó
Giới thiệu diễn giả
- Một lập trình viên từng viết mã C++ cho hệ thống hàng không vũ trụ và thực hiện các buổi trình diễn cho Không quân
- Phần trình bày dựa trên kinh nghiệm thực tế dùng C++ trong các hệ thống có yêu cầu an toàn rất cao
- Sử dụng MFD (màn hình đa chức năng) tự chế gồm X-Plane 12, web API, giao diện Python và backend C++ làm môi trường demo
Phần mềm bay và môi trường không cho phép thất bại
- Với ứng dụng thông thường, crash chỉ dẫn tới khởi động lại, nhưng trong môi trường tiêm kích và tên lửa ở Mach 1, một lần lỗi có thể lập tức trở thành thảm họa
- Câu “Ở Mach 1 không có thời gian để chờ garbage collector” nhấn mạnh yêu cầu thời gian thực
- Trong bối cảnh một dòng mã sai có thể gây hậu quả chết người, chính việc lựa chọn tính năng ngôn ngữ cũng phải trở thành một cơ chế an toàn
- Tai nạn nổ tên lửa Ariane 5 năm 1996 được đưa ra như ví dụ tiêu biểu
- Ngoại lệ xảy ra khi chuyển giá trị dấu phẩy động 64-bit của độ lệch ngang sang số nguyên 16-bit, và ngoại lệ này không được xử lý
- Ngôn ngữ đã phát sinh lỗi đúng theo đặc tả, nhưng hệ thống không xử lý được ngoại lệ đó, dẫn đến việc một tên lửa trị giá 500 triệu USD bị phá hủy ngay lập tức
- Lấy trường hợp này làm mốc, nhóm thiết kế F-35 chọn cách tiếp cận cắt bỏ ngay từ cấp độ tính năng ngôn ngữ để tránh lặp lại sai lầm tương tự
Lịch sử phần mềm quân sự và cuộc chiến ngôn ngữ
- Ở thời của tiêm kích đời đầu như F-4 Phantom, thực tế gần như chưa có phần mềm
- Máy tính ném bom gần với một cơ cấu cơ khí chính xác gồm bánh răng và cam hơn, và “mã” chính là hình dạng của cam kim loại
- Tình hình thay đổi ở dự án tuyệt mật tiêm kích chiếm ưu thế trên không của Hải quân VFX(F-14 Tomcat)
- Mãi về sau mới công khai rằng Garrett AiResearch đã thiết kế một bộ vi xử lý cho F-14 còn sớm hơn cả Intel 4004 vốn thường được xem là “bộ vi xử lý đầu tiên” trong sách giáo khoa
- Để điều khiển tối ưu cánh cụp cánh xòe (swing wing) của F-14, cần một bộ vi xử lý hiệu năng cao, trên đó nạp khoảng 2.500 dòng microcode để thực hiện các phép tính đa thức
- Sau đó, mỗi quân chủng lại chọn một ngôn ngữ khác nhau và tình trạng phân mảnh ngôn ngữ bắt đầu
- Không quân dùng Jovial(Jules Own Version of the International Algorithmic Language) thuộc họ ALGOL
- Hải quân không muốn dùng ngôn ngữ của Không quân nên chọn CMS-2 cho F-18
- Việc dùng các ngôn ngữ và kiến trúc phần cứng khác nhau khiến tái sử dụng mã và kiểm chứng gần như không thể thực hiện
- Đồng thời, quy mô phần mềm trên mỗi máy bay tăng theo cấp số nhân
- Các số liệu ví dụ được nêu gồm F-16A khoảng 125 nghìn dòng, B-1 khoảng 1 triệu dòng, và F-35 hiện đại khoảng 9 triệu dòng
- Báo cáo điều tra của Bộ Quốc phòng cho biết có hơn 450 ngôn ngữ lập trình đang được sử dụng, và hầu như không có ngôn ngữ nào có tiêu chuẩn đúng nghĩa
Việc áp đặt Ada và những giới hạn của nó
- Để giải quyết sự hỗn loạn đó, Bộ Quốc phòng tạo ra một ngôn ngữ bậc cao thống nhất là Ada và áp đặt nghĩa vụ sử dụng rất chặt chẽ
- Nếu một dự án mới muốn không dùng Ada thì phải chứng minh vì sao Ada không thể đáp ứng, nếu không thì không thể giành được hợp đồng
- Ada được giới thiệu như một ngôn ngữ rất phù hợp cho các lĩnh vực coi trọng an toàn và độ tin cậy
- Thiết kế của nó nhấn mạnh khả năng đảm bảo an toàn bộ nhớ và an toàn kiểu cho các hệ thống tối quan trọng như hàng không vũ trụ
- Nhưng từ thập niên 90, khoảng cách với thực tế bắt đầu lộ rõ
- Trong khi đó, Internet, Windows 95 và các game thương mại dựa trên C++ trở thành dòng chính
- Sinh viên và lập trình viên tự nhiên đổ về GCC miễn phí và C++ thay vì các trình biên dịch Ada đắt đỏ
- Trình biên dịch Ada có giá tới hàng nghìn USD nên cá nhân khó tiếp cận, kết quả là nguồn nhân lực chuyên Ada cũng dần thu hẹp
F-35 và sự ra đời của tiêu chuẩn JSF C++
- F-35 (Joint Strike Fighter) được thiết kế ngay từ đầu như một loại máy bay có tỷ trọng phần mềm cực lớn
- Các phép tính phức tạp như sensor fusion trở thành hạt nhân trong vận hành máy bay
- Lockheed Martin đã đề xuất với Bộ Quốc phòng việc cho phép sử dụng C++ để đáp ứng các yêu cầu đó
- Về thực chất đây là yêu cầu “nới” chính sách bắt buộc dùng Ada, và để thuyết phục được thì cần có cách kiểm soát rủi ro của C++
- Trong quá trình này, nhà sáng lập C++ Bjarne Stroustrup cũng được nhắc tới là đã tham gia cố vấn và góp phần vào việc thiết kế các quy tắc JSF C++
- Ông cho biết mình trực tiếp góp tay xây dựng các quy tắc JSF và tự nhận rằng vì thế có thể “thiên vị” với tiêu chuẩn này
- Ý tưởng cốt lõi giống với thẻ “remove before flight”
- Giống như chiếc thẻ phải tháo ra trước khi cất cánh, các tính năng nguy hiểm của C++ bị loại bỏ ở cấp ngôn ngữ để chỉ dùng một tập con có thể dự đoán được
- Nhờ vậy có thể đạt mức an toàn gần Ada trong khi nhà phát triển vẫn tận dụng được một phần sức biểu đạt của C++
Phần cứng thực tế và phép so sánh với GameCube
- Các block đầu của F-35 sử dụng máy tính nhiệm vụ dựa trên bộ xử lý Motorola G4 PowerPC
- Thông tin này đã được công khai trong bài viết của Aviation Today năm 2003 và các nguồn tương tự
- GameCube cũng dùng bộ xử lý dòng PowerPC, nên đây là một phép so sánh thú vị ở chỗ phần cứng cùng thế hệ tương tự ở mức tập lệnh
- Nếu muốn khớp thế hệ chính xác hơn thì có thể có máy console khác gần hơn, nhưng để hiểu nguyên lý thì ví dụ GameCube là đủ
Môi trường demo JSF C++: X-Plane 12 + MFD
- Dựa trên X-Plane 12, video xây dựng môi trường mô phỏng bay với addon F-35B của AOA Simulations
- Dùng web API mới của X-Plane để đăng ký dữ liệu bay thời gian thực rồi hiển thị lên MFD
- Frontend được viết bằng Python, còn backend là plugin C++, qua đó trình diễn so sánh giữa mã tuân thủ và mã vi phạm quy tắc JSF
- Hiển thị nhiều loại thông tin như độ cao, tốc độ, gió, phong bì bay, dữ liệu dẫn đường... từ kết quả tính toán bằng C++
- Trong lúc bay, video cố ý chạy mã C++ không chuẩn ném ngoại lệ để cho thấy MFD bị sập và chuyến bay phát sinh vấn đề, rồi từng bước áp dụng quy tắc JSF để khắc phục
Ba ràng buộc cốt lõi của JSF: ngoại lệ, đệ quy, bộ nhớ động
- Ba ràng buộc cốt lõi được nhấn mạnh trong tiêu chuẩn JSF C++ là ngoại lệ(Exception), đệ quy(Recursion), cấp phát bộ nhớ động
- Ngoài ra còn có giới hạn trên cho Cyclomatic Complexity(độ phức tạp phân nhánh) của hàm
1) Cấm ngoại lệ – AV Rule 208
- JSF AV Rule 208: “không được sử dụng ngoại lệ(exceptions shall not be used)”
- Cấm hoàn toàn các từ khóa liên quan đến ngoại lệ như try, catch, throw
- Lý do cốt lõi là tính bất định của luồng điều khiển
- Như Ariane 5, nếu ngoại lệ xảy ra mà thiếu xử lý hoặc lệch thời điểm thì toàn bộ hệ thống có thể sụp đổ theo cách không thể dự đoán
- Bjarne nhìn chung ủng hộ xử lý ngoại lệ trong C++ hiện đại, nhưng giải thích rằng vào thời điểm JSF được thiết kế, độ trưởng thành của công cụ và khả năng đảm bảo thời gian thực chưa đủ để hỗ trợ ngoại lệ
“JSF++ dành cho ứng dụng hard real-time và safety-critical (điều khiển bay), nên nếu tính toán mất quá lâu thì con người có thể thiệt mạng, và với ngoại lệ thì không thể đảm bảo thời gian đáp ứng”
- Thay cho ngoại lệ, JSF dùng mã trả về(return code)
- Trong ví dụ tính density altitude, mỗi tình huống lỗi sẽ đặt một mã trả về khác nhau và phía gọi sẽ diễn giải, xử lý mã đó
- Dù tính toán thất bại hay quá thời gian, toàn bộ chương trình không bị sập mà phía gọi vẫn có thể biểu diễn an toàn trạng thái “lỗi”
2) Cấm đệ quy – AV Rule 119
- AV Rule 119 cấm việc hàm gọi chính nó trực tiếp hoặc gián tiếp, tức là đệ quy
- Vì mỗi lần gọi đệ quy lại chồng thêm một stack frame mới, rất khó biết trước giới hạn độ sâu tối đa nên rủi ro stack overflow tăng cao
- Ví dụ được dùng là hệ số nhị thức(binomial coefficient) trong phép tính sân bay thay thế khi lập kế hoạch bay
- Ở phiên bản không chuẩn, dùng cài đặt đệ quy theo dạng
C(n, k) = C(n-1, k-1) + C(n-1, k) - Cách này khiến độ sâu lời gọi thay đổi theo đầu vào, nên khó dự đoán giới hạn bộ nhớ
- Ở phiên bản không chuẩn, dùng cài đặt đệ quy theo dạng
- Ở phiên bản tuân thủ JSF, phép tính tương tự được đổi sang cài đặt lặp(iterative) dựa trên vòng lặp
- Mã dài hơn và kém thanh lịch hơn, nhưng vì không tự gọi lại nên vẫn cho cùng kết quả mà không dùng đệ quy
- Nhờ đó độ sâu lời gọi hàm và giới hạn dùng bộ nhớ dễ được suy luận tĩnh hơn
3) Cấm cấp phát bộ nhớ động – AV Rule 206
- AV Rule 206: sau khi khởi tạo thì không được cấp phát hay giải phóng bộ nhớ nữa
- Cấm cấp phát trên heap trong lúc chạy như
new,delete, haynewnội bộ thông qua smart pointer
- Cấm cấp phát trên heap trong lúc chạy như
- Có hai lý do chính
- Cấp phát trên heap mang theo tính bất định về thời gian, không biết sẽ mất bao lâu
- Khi heap bị phân mảnh(fragmentation), dù tổng dung lượng còn đủ vẫn có thể không tìm được khối liên tục đủ lớn và việc cấp phát sẽ thất bại
- Ví dụ minh họa là đoạn mã không chuẩn tạo bộ đệm lịch sử IAS(tốc độ khí cụ) cho tính toán gust bằng
std::unique_ptr+ mảng động- Đây là dạng cấp phát mảng mới trong lúc chạy nên vi phạm quy tắc JSF
- Ở phiên bản tuân thủ JSF, thay vào đó dùng mảng kích thước cố định với kích thước tối đa được định nghĩa bằng hằng số
- Định nghĩa các hằng như
MAX_IAS_HISTORY, chỉ cấp phát một lần khi khởi tạo rồi xoay vòng chỉ số để sử dụng - Nhờ vậy trong lúc chạy không phát sinh cấp phát bổ sung nào, đảm bảo tính dự đoán được về thời gian và bộ nhớ
- Định nghĩa các hằng như
4) Giới hạn Cyclomatic Complexity – AV Rule 3
- AV Rule 3 quy định Cyclomatic Complexity(độ phức tạp phân nhánh) của một hàm không được vượt quá 20
- Bản thân khai báo hàm tính 1 điểm, còn if, while, for, switch, toán tử logic AND/OR... đều cộng thêm 1 vào độ phức tạp
- Với ví dụ cài đặt lặp của hệ số nhị thức, video cho thấy từng if, phép logic và vòng for làm tăng điểm độ phức tạp như thế nào
- Vì độ phức tạp càng cao thì việc kiểm thử, kiểm chứng và phân tích càng khó, nên mục tiêu của tiêu chuẩn là giữ nó dưới một ngưỡng nhất định
Di sản của JSF: NASA F-Prime, MISRA, AutoSAR
- Các ý tưởng của tiêu chuẩn JSF C++ sau đó lan sang những lĩnh vực an toàn cao khác
- Framework phần mềm bay F-Prime của NASA được công bố năm 2017 và chia sẻ các quy tắc như cấm cấp phát bộ nhớ động, cấm ngoại lệ, cấm đệ quy
- Trong ngành ô tô cũng xuất hiện xu hướng tương tự
- Các tiêu chuẩn như MISRA C++, AutoSAR(Automotive Open System Architecture) đưa ra các quy tắc an toàn cho phần mềm ô tô
- Hướng dẫn AutoSAR C++14 được nhắc là có tham chiếu rõ ràng tới JSF, cho thấy ảnh hưởng của JSF đã lan tới cả phần mềm xe hơi
- Khi ô tô hiện đại trên thực tế gần như là “máy tính gắn bánh xe”, các tập con ngôn ngữ và quy tắc mã hóa như vậy trở thành nền tảng cốt lõi nâng đỡ an toàn
Kết luận: Nếu dùng C++ ngày nay thì nên theo gì
- Tiêu chuẩn JSF C++ được xem như một thành tựu kỹ thuật của thời đó: thu hẹp một ngôn ngữ phức tạp thành tập con có thể dự đoán được để đạt mức an toàn đủ cho điều khiển bay trên tiêm kích
- Đồng thời, Bjarne Stroustrup khuyến nghị các nhà phát triển ngày nay nên theo C++ Core Guidelines và C++ hiện đại
- Vì ngôn ngữ C++ và toolchain đã phát triển mạnh trong vài thập kỷ qua, tạo ra nhiều điều kiện để dùng an toàn cả ngoại lệ lẫn smart pointer
- Dù vậy, JSF vẫn là một ví dụ quan trọng về cách kiểm soát ngôn ngữ bằng việc “loại bỏ” thay vì bổ sung
- Bài trình bày kết lại bằng thông điệp rằng trong thiết kế hệ thống an toàn cao, điều quan trọng không chỉ là thêm gì, mà là đưa những gì vào danh sách remove before flight
8 bình luận
Có lẽ vì là mục đích quân sự nên kết quả của việc cân bằng giữa cấu hình phần cứng thấp và các tính năng cao cấp đã dẫn đến việc chọn C++.
gnat-llvmdựa trên llvm nữa. Cũng có cả IDE mã nguồn mở.Sinh viên và lập trình viên không học là vì đây là ngôn ngữ của Bộ Quốc phòng và nhu cầu thấp, chứ có lẽ không phải vì công cụ đắt đỏ.
Nhìn chung, đây là nội dung về các kỹ thuật viết mã có tính dự đoán được.
Chỉ là C++ được dùng làm ví dụ, nhưng ở các ngôn ngữ khác, những phần còn gây vấn đề hơn như GC cũng tương tự, nên khá đáng tiếc là bài viết có thể bị hiểu như đang bàn về giới hạn của C++.
Nếu đã không dùng các kỹ thuật như cấp phát động hay xử lý ngoại lệ của C++, thì vẫn còn băn khoăn liệu dùng C và viết theo các nguyên tắc trên có phải sẽ dễ và nhanh hơn nhiều hay không.
Đúng vậy, tôi cũng không hiểu vì sao lại là C++ chứ không phải C.
C++ hiện đại quả thực rất ổn định, nhưng nếu không nhất thiết phải là C++ thì có lẽ cũng nên cân nhắc những ngôn ngữ khác ổn định hơn.
Hãy dùng cú pháp RUST một cách NGHIÊM NGẶT!
Ý kiến Hacker News
Dài 142 trang, có thể thấy những ràng buộc nào tồn tại trong phát triển phần mềm máy bay thực tế
Tuy vậy, tôi tò mò về các ngoại lệ của những quy tắc “shall”. Trong các dự án lớn như vậy, các trường hợp ngoại lệ mới cho thấy tính hiệu lực thực sự của tiêu chuẩn
Vào năm 2005 thì điều này có lẽ ổn, nhưng tôi tò mò không biết sẽ áp dụng thế nào trong các môi trường như drone dựa trên AI ngày nay
Đặc biệt những chỗ như cấm
stdio.hnghe khá lạ, nhưng đọc kỹ thì lại thấy “ừ, cũng có lý”a = a;mà tôi từng thấy trong mã MISRAĐó là một mẹo để khỏi phải xóa tham số không dùng đến, nhưng tôi vẫn nghi ngờ liệu những quy tắc kiểu này có thực sự đảm bảo chất lượng mã tốt hay không
Bộ hướng dẫn JSF là tài liệu từ năm 2005 nên có giới hạn của thời đại
Việc Bjarne Stroustrup gần đây đưa ra khái niệm “C++ profile” cũng khá thú vị
Suy cho cùng, các style guide kiểu này có thể cũng là vấn đề của gu thẩm mỹ
(void)a;Thứ thực sự đảm bảo an toàn là chất lượng thiết kế và cấu trúc fail-safe
_ = a;Cũng có issue liên quan
Thay vào đó, chúng đóng vai trò cung cấp một chuẩn chung để tham chiếu khi review
Cốt lõi là đảm bảo nhiệm vụ (mission assurance)
Nếu dùng stack hay heap thì địa chỉ bộ nhớ của biến sẽ thay đổi, và nếu một ô nhớ cụ thể bị lỗi thì sẽ phát sinh vấn đề
Nếu mọi biến đều có địa chỉ cố định, thì chỉ cần dời ô bị lỗi bằng bản vá là có thể tiếp tục nhiệm vụ
Biến cục bộ, tham số, địa chỉ trả về v.v. cuối cùng vẫn cần stack
Đệ quy cũng trở nên bất khả thi, và biến tạm cũng bị hạn chế
Vì vậy lập luận này không thực tế
Có thể cố định phạm vi địa chỉ của stack và heap, nhưng tôi vẫn nghi ngờ liệu đây có phải là một lý do đủ thuyết phục hay không
if,else ifđều phải cóelsehoặc có chú thích”Tôi cũng hay để lại log kiểu “trường hợp này tuyệt đối không nên xảy ra”
Trong các hệ thống lớn, kiểu ghi log tình huống ngoại lệ này rất hữu ích cho việc gỡ lỗi
Mọi trường hợp đều phải được xử lý tường minh, nên nếu có thêm giá trị enum thì trình biên dịch sẽ cảnh báo
_STOPhoặc_CRASHđể dừng debug ngay lập tứcNó có tác dụng ép phải sửa lỗi ngay tại chỗ
Tóm lại là vì “thiếu lập trình viên Ada và thiếu toolchain”
Nhưng hiện nay sự cởi mở với đa dạng ngôn ngữ đã lớn hơn, nên có vẻ Ada có thể được chấp nhận hơn
Việc NVidia chọn SPARK cũng trông như dấu hiệu hồi sinh của Ada
Nếu DoD bắt buộc dùng Ada thì các trường đại học và doanh nghiệp đã phải đi theo
Suy cho cùng thì ngôn ngữ có thể học được, và nếu dùng Ada thì có lẽ độ tin cậy của F-35 cũng đã cao hơn
Như AdaCore, GHS, PTC ApexAda, DDC-I, Irvine, OC Systems, RR Software
Trước đây trình biên dịch Ada là tùy chọn trả phí, còn C/C++ thì có sẵn mặc định nên trường học và doanh nghiệp đã chọn C++
AdaCore đã đóng góp rất lớn cho tiêu chuẩn hóa ISO và sự lan rộng của mã nguồn mở
Trước đây nó bị chỉ trích quá mức, nhưng bây giờ lại thấy khá hấp dẫn
Cấu trúc tệp và cờ build khá phức tạp, và trong bảng xếp hạng ngôn ngữ của RedMonk cũng không có Ada
Một vài tính năng khá thú vị, nhưng trải nghiệm ngôn ngữ hiện đại như Rust thì không phải
Các khung chứng nhận như DO-178C mới là quan trọng
Thậm chí đây có khi còn là cách đúng đắn để viết mã độ tin cậy cao
Bao quát nhiều chủ đề như reverse engineering, obfuscation, compiler
Tôi đã nghĩ là những điều như thế này mà cũng phải viết ra rõ ràng sao
Là Lockheed Martin tự làm hay là sản phẩm thương mại