- Amazon Web Services (AWS) xem tính đúng đắn của dịch vụ là giá trị cốt lõi và tích hợp nhiều dạng phương pháp hình thức vào quy trình phát triển
- Thông qua các công cụ đặc tả hình thức như TLA+ và ngôn ngữ P, AWS có thể phát hiện sớm các lỗi tinh vi và vẫn bảo đảm độ tin cậy ngay cả với những tối ưu hóa táo bạo
- AWS cũng vận hành rộng rãi các phương pháp hình thức hạng nhẹ như kiểm thử dựa trên thuộc tính, mô phỏng xác định và fuzzing liên tục
- Thông qua các công cụ tiêm lỗi như Fault Injection Service, AWS tự động hóa việc xác minh độ tin cậy, bao gồm cả các tình huống xảy ra sự cố
- Dù rào cản đào tạo và độ phức tạp của công cụ vẫn còn, sự phổ biến của AI và các công cụ tự động hóa được kỳ vọng sẽ thúc đẩy việc áp dụng rộng rãi hơn
Chiến lược bảo đảm tính đúng đắn hệ thống của AWS
Amazon Web Services (AWS) hướng tới mục tiêu cung cấp các dịch vụ có độ tin cậy cao mà khách hàng có thể hoàn toàn tin tưởng.
Để làm được điều đó, AWS theo đuổi việc duy trì các tiêu chuẩn về bảo mật, độ bền, tính toàn vẹn và tính sẵn sàng, đồng thời đặt khái niệm tính đúng đắn hệ thống ở vị trí trung tâm.
Kể từ khi trường hợp áp dụng phương pháp hình thức của AWS được giới thiệu trên Communications of the ACM năm 2015, cách tiếp cận này đã đóng vai trò quan trọng trong việc vận hành thành công các dịch vụ cốt lõi.
Ở trung tâm là TLA+, một ngôn ngữ đặc tả hình thức do Leslie Lamport phát triển.
Kinh nghiệm áp dụng TLA+ tại AWS cho phép phát hiện các lỗi rất nhỏ ngay từ giai đoạn đầu phát triển, những lỗi mà kiểm thử truyền thống khó bắt được.
Ngoài ra, ngay cả khi thực hiện các tối ưu hóa hiệu năng mạnh tay, AWS vẫn có thể bảo đảm tính ổn định và độ tin cậy thông qua xác minh hình thức.
Cách đây 15 năm, AWS mới chỉ dừng ở mức cơ bản như unit test tại thời điểm build và một số integration test hạn chế, nhưng sau đó đã áp dụng toàn diện cả các cách tiếp cận hình thức lẫn bán hình thức.
Sự thay đổi này không chỉ cải thiện tính đúng đắn mà còn góp phần xác minh các tối ưu hóa ở cả mức cao và mức thấp, tăng tốc độ phát triển và giảm chi phí.
Tại AWS, ngoài chứng minh hình thức và kiểm chứng mô hình, các kỹ thuật như kiểm thử dựa trên thuộc tính, fuzzing và giám sát thời gian chạy cũng được xem là một phần của phương pháp hình thức.
Sự xuất hiện của ngôn ngữ lập trình P
Ban đầu, TLA+ có ưu thế là một cách mô tả trừu tượng rất mạnh, nhưng với nhiều lập trình viên, rào cản tiếp cận do ký pháp toán học là khá lớn.
Vì vậy, AWS đã đưa vào sử dụng ngôn ngữ P, cung cấp cách tiếp cận dựa trên máy trạng thái mà các nhà phát triển dễ làm quen hơn.
Ngôn ngữ P cung cấp phương pháp mô hình hóa bằng máy trạng thái để thiết kế và phân tích hệ thống phân tán.
Đây là khái niệm quen thuộc với các nhà phát triển Amazon làm việc với kiến trúc SOA dựa trên microservices.
Từ năm 2019, P được AWS phát triển và quản lý như một dự án mã nguồn mở chiến lược.
Các nhóm dịch vụ lớn như Amazon S3, EBS, DynamoDB, Aurora, EC2, IoT sử dụng P để xác minh tính đúng đắn trong thiết kế hệ thống.
Khi chuyển S3 sang tính nhất quán read-after-write mạnh, AWS đã mô hình hóa và xác minh giao thức bằng P, từ đó loại bỏ lỗi ngay ở giai đoạn đầu thiết kế và phản ánh các tối ưu hóa một cách an toàn.
Năm 2023, nhóm P của AWS phát triển công cụ PObserve, cho phép xác minh tính đúng đắn của hệ thống phân tán cả trong môi trường kiểm thử lẫn vận hành thực tế.
PObserve trích xuất log thực thi để có thể hậu kiểm xem hệ thống có hoạt động đúng theo đặc tả hay không, đồng thời liên kết hiệu quả đặc tả ở giai đoạn thiết kế với phần triển khai mã thực tế.
Mở rộng các phương pháp hình thức hạng nhẹ
Kiểm thử dựa trên thuộc tính
Kỹ thuật hình thức hạng nhẹ tiêu biểu nhất là kiểm thử dựa trên thuộc tính.
Ví dụ, nhóm phát triển ShardStore của S3 sử dụng kết hợp kiểm thử dựa trên thuộc tính, fuzzing dựa trên độ bao phủ mã, tiêm lỗi và tối giản phản ví dụ xuyên suốt toàn bộ chu kỳ phát triển.
Cách làm này gắn với các đặc tả tính đúng đắn do chính nhà phát triển viết ra, đồng thời cải thiện đáng kể hiệu quả gỡ lỗi.
Mô phỏng xác định
Kiểm thử bằng mô phỏng xác định chạy hệ thống phân tán trong một trình mô phỏng đơn luồng, cho phép kiểm soát mọi yếu tố ngẫu nhiên như lập lịch, thời gian và thứ tự thông điệp.
Phương pháp này được áp dụng theo nhiều cách khác nhau, như kiểm thử các kịch bản lỗi và thành công cụ thể, điều chỉnh thứ tự gây ra lỗi, hay mở rộng fuzzing.
Nhờ đó, việc xác minh hành vi như độ trễ và lỗi của hệ thống có thể được thực hiện sớm ngay từ giai đoạn build, đồng thời mở rộng phạm vi kiểm thử.
AWS đã công khai mã kiểm thử thời điểm build này qua các dự án mã nguồn mở shuttle và turmoil.
Fuzzing liên tục
Fuzzing liên tục, đặc biệt là tạo đầu vào quy mô lớn dựa trên độ bao phủ mã, rất hiệu quả trong việc xác minh tính đúng đắn hệ thống ở giai đoạn kiểm thử tích hợp.
Ví dụ, khi phát triển Aurora Limitless Database, AWS đã fuzz các truy vấn SQL và giao dịch để kiểm chứng tính đúng đắn của logic phân vùng bằng cách tạo ra số lượng lớn schema, tập dữ liệu và truy vấn ngẫu nhiên.
Kết quả được so sánh với hành vi của engine non-sharded hoặc với các phương pháp như SQLancer.
Việc kết hợp fuzzing và tiêm lỗi giúp xác minh các thuộc tính cốt lõi của cơ sở dữ liệu như tính nguyên tử, tính nhất quán và tính cô lập.
Một số thuộc tính như giao dịch được tạo tự động và tính cô lập được bảo đảm thông qua hậu kiểm dựa trên lịch sử thực thi.
Tiêm lỗi thông qua Fault Injection Service
Năm 2021, AWS ra mắt Fault Injection Service (FIS), cho phép cả khách hàng nhanh chóng thử nghiệm nhiều kịch bản lỗi khác nhau như lỗi API, gián đoạn I/O và sự cố instance trong môi trường thực tế hoặc môi trường kiểm thử.
Qua đó, AWS có thể bảo đảm tính sẵn sàng của kiến trúc, kiểm tra khả năng phục hồi khi sự cố xảy ra, thu hẹp chênh lệch mật độ lỗi cao ở các trường hợp lỗi và phát hiện sớm những vấn đề nghiêm trọng có khả năng xảy ra.
FIS được sử dụng rộng rãi không chỉ bởi khách hàng AWS mà còn trong nội bộ Amazon; riêng trong quá trình chuẩn bị cho Prime Day đã có 733 thí nghiệm được tiến hành.
Tiêm lỗi còn hiệu quả hơn khi kết hợp với đặc tả hình thức.
Sau khi viết hành vi mong đợi dưới dạng đặc tả hình thức, kết quả gây lỗi thực tế có thể được đối chiếu với đặc tả đó để phát hiện nhiều lỗi hơn so với cách kiểm tra log hay chỉ số đơn thuần trước đây.
Metastability và hành vi phát sinh của hệ thống
Trong hệ thống phân tán, ngày càng có nhiều trường hợp rơi vào trạng thái bất thường “không thể tự phục hồi” (metastable) do tải quá mức, cạn bộ nhớ đệm và các nguyên nhân tương tự.
Ở trạng thái này, chỉ giảm tải đơn thuần cũng không thể khôi phục hoạt động bình thường, và việc ứng phó còn khó hơn các trường hợp lỗi thông thường.
Phần lớn logic retry-timeout cũng là nguyên nhân gây ra hiện tượng này.
Các đặc tả hình thức truyền thống tập trung vào tính an toàn và tính tiến triển, nhưng metastability đòi hỏi phải xem xét cả nhiều hành vi phát sinh khác ngoài các yếu tố đó.
Dựa trên các mô hình đặc tả như TLA+ và P, AWS tiến hành mô phỏng sự kiện rời rạc để phân tích có hệ thống cả các đặc tính xác suất như khả năng đạt SLA hiệu năng hay phân bố độ trễ.
Sự cần thiết của chứng minh hình thức
Ở một số ranh giới bảo mật (quyền hạn, ảo hóa, v.v.), các chứng minh ở cấp độ toán học là bắt buộc, vượt xa kiểm thử đơn thuần.
Ví dụ, ngôn ngữ chính sách phân quyền Cedar mà AWS đưa vào năm 2023 được tối ưu cho chứng minh tự động và xác minh hình thức dựa trên Dafny, đồng thời thông qua mã nguồn công khai và quy trình hiệu chỉnh, toàn bộ người dùng cũng có thể tự mình xác minh.
Ngoài ra, các thuộc tính bảo mật cốt lõi của Firecracker VMM đang được chứng minh bằng các công cụ phân tích mã Rust như Kani.
Bằng cách sử dụng rộng rãi các mô hình và đặc tả hình thức ở nhiều thời điểm khác nhau như thiết kế, triển khai, vận hành và chứng minh, AWS tận dụng chúng để bảo đảm tính đúng đắn phần mềm cũng như mở rộng giá trị cho doanh nghiệp và khách hàng.
Các tác động bổ sung vượt ra ngoài tính đúng đắn
Phương pháp hình thức đóng vai trò quan trọng đối với cả độ tin cậy và cải thiện hiệu năng.
Ví dụ, AWS đã xác minh giao thức commit của Aurora bằng P và TLA+, vừa giảm số vòng round-trip mạng vừa bảo đảm an toàn.
Khi tối ưu thuật toán mã hóa RSA cho ARM Graviton 2, AWS đã chứng minh tính đúng đắn toán học của phép biến đổi trong HOL Light, qua đó đạt được hiệu quả thực tế là cải thiện đồng thời hiệu năng và chi phí hạ tầng.
Thách thức và cơ hội trong tương lai
Trong 15 năm qua, AWS đã mở rộng đáng kể việc áp dụng các phương pháp hình thức/bán hình thức trong công nghiệp, nhưng các rào cản triển khai thực tế như đường cong học tập, nhu cầu về chuyên gia và tính hàn lâm của công cụ vẫn còn tồn tại.
Ngay cả các kỹ thuật như kiểm thử dựa trên thuộc tính hay mô phỏng xác định cũng vẫn còn xa lạ với nhiều lập trình viên.
Do rào cản tiếp cận về mặt đào tạo đã tồn tại từ bậc đại học, việc phổ biến công cụ và phương pháp luận cũng như ứng dụng trong thực tế diễn ra khá chậm.
Các đặc tính phát sinh của hệ thống quy mô lớn như metastability cũng mới chỉ ở giai đoạn nghiên cứu ban đầu.
Trong tương lai, AI/mô hình ngôn ngữ lớn được kỳ vọng sẽ hỗ trợ việc viết mô hình và đặc tả hình thức, từ đó nâng cao mạnh mẽ khả năng tiếp cận của người làm thực tế trong thời gian ngắn.
Kết luận
Để xây dựng phần mềm vững chắc và an toàn, cần nhiều biện pháp khác nhau nhằm bảo đảm tính đúng đắn hệ thống.
Ngoài các kỹ thuật kiểm thử tiêu chuẩn, AWS còn áp dụng toàn diện model checking, fuzzing, kiểm thử dựa trên thuộc tính, kiểm thử tiêm lỗi, mô phỏng xác định/dựa trên sự kiện và xác minh lịch sử thực thi.
Các đặc tả và phương pháp hình thức đóng vai trò như một oracle kiểm thử quan trọng trong quy trình phát triển của AWS, và thông qua việc chứng minh hiệu quả thực tiễn lẫn kinh tế, chúng đã trở thành một lĩnh vực đáng để đầu tư.
1 bình luận
Ý kiến trên Hacker News
Tôi muốn nói về cách kiểm thử mô phỏng tất định. Ở AWS, họ chạy hệ thống phân tán trong một trình mô phỏng đơn luồng, đồng thời kiểm soát mọi yếu tố không tất định như lập lịch luồng, thời gian, thứ tự chuyển phát thông điệp, v.v. Sau đó họ viết các bài kiểm thử tương ứng với những kịch bản thất bại hoặc thành công cụ thể, còn tính không tất định trong hệ thống thì do framework kiểm thử kiểm soát. Lập trình viên có thể chỉ định một thứ tự cụ thể từng gây ra lỗi trong quá khứ. Bộ lập lịch còn có thể mở rộng sang fuzzing thứ tự hoặc thậm chí duyệt mọi thứ tự có thể. Tôi tò mò không biết có thư viện nào mã nguồn mở triển khai kiểu này theo cách không phụ thuộc ngôn ngữ hay không. Ý tưởng là cần một công cụ middleware có thể làm cho cả networking, storage, v.v. bên trong container trở nên "tất định" tại thời điểm kiểm thử. antithesis gần như làm đúng vai trò đó, nhưng tôi vẫn chưa thấy bản mã nguồn mở. Nếu viết test tốt thì có thể giải quyết phần nào bằng cách stub những thứ như I/O, nhưng không thể đảm bảo ai cũng viết test tốt. Tôi nghĩ sẽ rất hay nếu có thể cung cấp tính tất định ở một tầng cao hơn phía trên ứng dụng. Mặt khác, tôi kỳ vọng AI có thể thật sự tỏa sáng trong kiểm thử. Bộ ba prompt (yêu cầu) - triển khai test - AI - mã thực thi có thể ăn khớp với nhau một cách lý tưởng. Tôi hy vọng AI sẽ giúp formal verification trở nên dễ tiếp cận hơn để làm thế giới phần mềm chặt chẽ hơn nữa
Có hai khó khăn trong việc phổ biến kỹ thuật kiểm thử mô phỏng tất định (DST). Thứ nhất, trước đây phải đặt toàn bộ hệ thống trực tiếp lên một framework mô phỏng cụ thể và không được có phụ thuộc khác. Thứ hai, nếu việc sinh đầu vào và khám phá quá yếu thì test sẽ chỉ giả vờ là mọi thứ đều qua, trong khi thực tế không có kiểm chứng gì đáng kể. antithesis đang cố giải quyết cả hai vấn đề này nhưng vẫn còn rất nhiều khó khăn. Hầu như chưa có nơi nào có một cách chắc chắn để áp dụng tính tất định cho bất kỳ phần mềm nào. Dự án Hermit của Facebook cũng từng thử với Linux userspace tất định nhưng cuối cùng đã dừng lại. Máy tính tất định là một nền tảng kỹ thuật cực kỳ hữu ích không chỉ cho kiểm thử, và tôi nghĩ sớm muộn gì cũng sẽ có người công bố nó dưới dạng mã nguồn mở
Tôi nghĩ việc chạy QEMU ở chế độ mô phỏng 100% với một luồng duy nhất để có được một cỗ máy tất định là tương đối dễ. Nhưng thứ thực sự ta muốn là thực thi tất định có thể "điều khiển được", và điều này khó hơn rất nhiều. Nếu muốn nhiều tiến trình hoạt động theo một kịch bản chỉ định, thì độ khó đặc biệt cao ở cấp CPU và OS scheduler. Việc tạo ra chính môi trường không phụ thuộc ngôn ngữ cũng khó, và rất dễ bị sa lầy vào các chi tiết nhỏ. Tôi cũng từng làm một hệ thống đơn giản để cho nhiều JVM thread chạy lockstep tại những thời điểm hành vi cụ thể, xử lý I/O và system time bằng stub và điều khiển. Nhờ vậy tôi đã kiểm thử được nhiều tương tác khác nhau giữa các thành phần bất đồng bộ, lỗi I/O, retry, v.v., và bắt được những bug đau đầu trước khi lên production. Tuy nhiên, cách đó chỉ khả thi vì tôi đơn giản hóa một số điểm đồng bộ cụ thể chứ không điều khiển toàn bộ hệ thống. Những data race thông thường do lỗi đồng bộ thì cách này khó bắt được
Chia sẻ tài liệu chính thức về phương pháp kiểm thử của FoundationDB và video trình bày trên YouTube
Nếu là ngôn ngữ có thể debug bằng gdb, tôi khuyên dùng dự án https://rr-project.org/
Tôi nhớ đã từng xem một bài trình bày của Joe Armstrong về việc kiểm thử Dropbox bằng property testing
Tôi nghĩ S3 là một trong những phần mềm ấn tượng nhất mà tôi từng thấy. Việc vài năm trước họ bổ sung tính nhất quán đọc-sau-ghi mạnh cho toàn bộ hệ thống S3 cũng thực sự là đỉnh cao của kỹ nghệ phần mềm liên kết bài blog
Tôi từng trực tiếp làm về lifecycle của S3, và thời điểm đó trùng với lúc team index đang thiết kế lại kiến trúc để cung cấp tính nhất quán này. Nhìn từ bên ngoài thì S3 đã rất đáng nể, nhưng bên trong còn ấn tượng vượt xa tưởng tượng, cả về triển khai lẫn cấu trúc tổ chức
Google Cloud Storage thực ra đã có tính năng này (nhất quán mạnh) từ rất lâu trước S3. Nhìn tổng thể thì tôi có cảm giác GCS là một sản phẩm bài bản và được xây dựng chỉn chu hơn một chút
Tôi đồng cảm với con số 92% (phần lớn sự cố cụm bắt đầu từ những lỗi nhỏ nhặt). Phần lớn không phải là các thảm họa hoành tráng, mà là những lần retry "chẳng có gì to tát" tích tụ trạng thái dần dần, rồi cuối cùng bùng nổ thành sự cố diện rộng lúc 2 giờ sáng. Việc dành nhiều thời gian kỹ thuật hơn cho những lỗi khó thấy là rất quan trọng
Tôi thấy đây là một bài viết thực sự thú vị. Việc dùng state machine để xây dựng infrastructure control plane là điều bắt buộc. Tôi không chắc có thật sự cần P hay không. Bên tôi cũng đã xây control plane hạ tầng bằng Ruby hơn 13 năm và nó chạy rất tốt bài blog chia sẻ kinh nghiệm liên quan
Tôi từng có thắc mắc về ngôn ngữ P. Trước đây có vẻ Microsoft từng dùng P để sinh mã C cho runtime của Windows USB stack và thực sự đưa vào sử dụng, nhưng giờ có vẻ họ không còn dùng nó để sinh mã production nữa. Tôi cũng từng để lại câu hỏi liên quan trên Hacker News liên kết câu hỏi. Nếu mã được sinh ra có thể đi vào cả kernel, thì trong môi trường cloud với điều kiện nhẹ hơn nhiều chắc chắn cũng có thể dùng được
Với người không xuất thân từ AWS và cũng không quen với TLA+ hay P như tôi, nếu có một ví dụ kiểu "hello world" thì có lẽ sẽ dễ hiểu hơn nhiều. Chỉ đọc bài viết thì đôi lúc nó giống một quá trình rất đau đớn, và khiến tôi nghĩ liệu đây có phải những vấn đề mà chỉ cần thiết kế và kiểm thử tốt là đủ bắt được không. Nếu có một ví dụ đơn giản thì sẽ dễ đánh giá hơn là họ thực sự đang làm gì
Có một ví dụ demo nhanh về TLA+ mà tôi rất thích liên kết gist. Đó là mô hình nhiều luồng cùng tăng một bộ đếm dùng chung theo cách không nguyên tử, và khi kiểm tra thuộc tính thì sẽ bắt được race condition. Trên thực tế rất khó phát hiện kiểu bug này chỉ bằng test. Hầu hết đặc tả TLA+ còn phức tạp hơn nhiều, nhưng ví dụ này rất hay để bắt lỗi đơn giản
Tôi đã trực tiếp dùng TLA nhưng từng thất vọng vì công cụ đồ họa không khớp tốt với tutorial. Bản thân TLA thì tôi vẫn muốn dùng, và từ xưa tôi đã thích công trình của Lamport (từ LaTeX đến các bài báo)
Tiền đề của việc dùng formal methods cuối cùng là chỉ dựa vào test thì tuyệt đối không thể bắt được mọi vấn đề
Tôi khuyên dùng kho lưu trữ GitHub TLA+ Examples chính thức. Nên bắt đầu từ những thứ đơn giản như bài toán DieHard
Test chứng minh tính đúng đắn của cách triển khai đối với một số instance cụ thể của vấn đề, còn formal verification thì chứng minh trên cả một lớp trường hợp. Ví dụ với một hàm trả về anagram, test chỉ xác nhận trên một vài cặp từ, nhưng để chứng minh tính đúng đắn với toàn bộ các cặp từ thì cần formal verification. Những trường hợp như undefined behavior hay bug thư viện cũng thường chỉ bị phát hiện trong quá trình formal verification
Với câu nhắc đến "các kỹ thuật bán hình thức hạng nhẹ như kiểm thử dựa trên thuộc tính, fuzzing, giám sát runtime", tôi thấy property-based testing và fuzzing đúng là các tập con của formal methods, nhưng xếp cả runtime monitoring vào nhóm kỹ thuật bán hình thức thì hơi quá tay
Trước đây tôi từng trao đổi với Leslie Lamport về Buridan's Principle và một số bài báo liên quan. Hôm nay tôi biết thêm rất nhiều về TLA+ và PlusCal từ trang cá nhân của ông ấy trang ví dụ Peterson. Việc người đã đưa toán học vào lập trình và gần như khai sinh lĩnh vực hệ thống đồng thời lại tạo ra ngôn ngữ thiết kế hệ thống (TLA+), rồi được dùng ở AWS và nhiều nơi khác, nghe cực kỳ tự nhiên. Tôi mong những người xây hệ thống phân tán sẽ dùng nhiều hơn những gì Lamport đã tạo ra. Với các hệ thống quy mô lớn, việc chứng minh tính đúng đắn là cực kỳ quan trọng
Claude Opus (Extended Thinking) rất hữu ích để chuyển mã hiện có sang đặc tả TLA+. Tôi đã có kinh nghiệm tìm ra nhiều bug khi dùng nó để xác minh các dự án Rust hoặc các thành phần lõi bằng C++. Các model khác thường hay vướng ở cú pháp và logic của đặc tả, còn Opus thì chạy mượt hơn nhiều
Không chỉ hệ thống lớn, mà cả những utility nhỏ nhưng quan trọng và được dùng rộng rãi trên toàn thế giới như SSH hay terminal cũng rất hưởng lợi từ việc chứng minh tính đúng đắn
Về phát biểu "chứng minh tính đúng đắn của hệ thống", thực ra không thể chứng minh toàn bộ. Model checker chỉ có thể cho biết rằng trong một không gian trạng thái hữu hạn, đặc tả đã nêu có thỏa mãn các thuộc tính hay không
Cá nhân tôi tò mò không biết có ai từng dùng FIS cho các thí nghiệm trên dịch vụ phân tán chưa. Tôi đang cân nhắc áp dụng nhưng chưa có kinh nghiệm trực tiếp với các thử nghiệm quy mô lớn
Tôi tự hỏi liệu Promela và SPIN có phải là ngôn ngữ ở mức trừu tượng cao hơn những gì bài viết đang nói đến không