Kiểm chứng hình thức là dùng logic và toán học để chứng minh một con chip hay một chương trình đúng với bản đặc tả trên mọi đầu vào có thể, thay vì chỉ thử một số trường hợp. Kiểm thử chỉ cho thấy có lỗi ở chỗ đã thử; chứng minh thì bao phủ cả những chỗ không ai nghĩ tới. Sau vụ lỗi phép chia của chip Intel Pentium năm 1994, các hãng chip đầu tư mạnh vào cách làm này, và ngày nay nó được dùng cho bộ xử lý, trình biên dịch, nhân hệ điều hành và các hệ thống điện toán đám mây.
Vì sao thử nhiều tới đâu cũng không đủ
Một bộ cộng 64 bit nhận hai số, mỗi số 64 bit, tức 2¹²⁸ cặp đầu vào — khoảng 3,4 × 10³⁸. Thử một tỉ tỉ (10¹⁸) cặp mỗi giây thì cũng cần khoảng 10¹³ năm. Với một chương trình có bộ nhớ, vòng lặp và nhiều luồng chạy xen kẽ, số trạng thái còn lớn hơn nữa.
Edsger Dijkstra từng viết, đại ý: kiểm thử có thể chỉ ra rằng chương trình có lỗi, nhưng không bao giờ chỉ ra được rằng nó không có lỗi. Về logic, đây là sự bất đối xứng quen thuộc: một phản ví dụ đủ bác bỏ "chương trình luôn đúng", nhưng bao nhiêu ví dụ đúng cũng không chứng minh được câu "với mọi đầu vào". Muốn có câu "với mọi", phải có chứng minh.
Bài học đắt giá: lỗi phép chia của Pentium (1994)
Năm 1994, Thomas Nicely, giáo sư toán ở Lynchburg College (Mỹ), đang tính toán trên các cặp số nguyên tố sinh đôi thì thấy kết quả lệch so với máy khác. Lần ngược lại, ông xác định thủ phạm là bộ chia số thực dấu phẩy động của chip Pentium. Ví dụ hay được nhắc nhất:
- Đúng: 4.195.835 ÷ 3.145.727 = 1,333820449…
- Pentium lỗi cho: 1,333739068…
Sai từ chữ số thứ năm. Nguyên nhân: thuật toán chia dùng một bảng tra, và vài ô trong bảng bị thiếu giá trị đúng. Những ô đó hiếm khi được chạm tới, nên hàng loạt bài kiểm thử trước khi xuất xưởng không phát hiện. Đầu năm 1995, Intel ghi nhận khoản chi phí 475 triệu đô-la cho việc thay chip.
Điều đáng nói: lỗi nằm trong một bảng hữu hạn, có thể kiểm được bằng lập luận chặt chẽ. Sau vụ này, các hãng chip đẩy mạnh kiểm chứng hình thức cho khối số học. Chẳng hạn, thuật toán chia của chip AMD K5 đã được chứng minh đúng bằng bộ chứng minh định lý ACL2 vào giữa thập niên 1990.
Hai cách làm chính
| Kiểm tra mô hình (model checking) | Chứng minh định lý (theorem proving) | |
|---|---|---|
| Ý tưởng | Máy duyệt hết mọi trạng thái của một mô hình hữu hạn, kiểm từng trạng thái có thoả tính chất không | Người và máy cùng viết một chứng minh logic, máy kiểm từng bước |
| Ưu điểm | Tự động; nếu sai thì đưa ra đúng chuỗi bước dẫn tới lỗi (phản ví dụ) | Xử lý được hệ vô hạn trạng thái, tính chất toán học sâu |
| Hạn chế | Số trạng thái bùng nổ khi hệ lớn | Tốn công người, cần chuyên môn cao |
| Ví dụ dùng | Giao thức, mạch điều khiển, phần mềm nhiều luồng | Khối số học dấu phẩy động, trình biên dịch, nhân hệ điều hành |
Cả hai đều dựa vào một thứ chung: đặc tả — mô tả chính xác bằng logic điều hệ thống phải làm. Một bộ giải SAT (xem bài riêng trong danh mục) thường là "động cơ" bên trong của cả hai.
Hai ví dụ giải đầy đủ
Ví dụ 1: chứng minh một vòng lặp bằng bất biến
Năm 1969 Tony Hoare đưa ra cách viết bộ ba Hoare {P} C {Q}: nếu điều kiện P đúng trước khi chạy lệnh C, và C chạy xong, thì Q đúng sau đó. Lấy chương trình tính tổng 1 + 2 + … + n (n là số nguyên không âm):
s = 0; i = 0;
while (i < n) { i = i + 1; s = s + i; }
Đặc tả: sau vòng lặp, s = n(n + 1)/2.
Chìa khoá là một bất biến vòng lặp: một câu đúng trước vòng lặp và vẫn đúng sau mỗi lượt. Chọn bất biến: s = i(i + 1)/2 và i ≤ n.
- Đúng lúc đầu. i = 0, s = 0: 0·1/2 = 0, đúng; 0 ≤ n, đúng.
- Giữ nguyên qua mỗi lượt. Giả sử trước lượt có s = i(i + 1)/2 và điều kiện lặp i < n. Sau lượt, i mới = i + 1 và s mới = i(i + 1)/2 + (i + 1) = (i + 1)(i + 2)/2 = i mới·(i mới + 1)/2. Còn i < n nên i mới ≤ n. Bất biến vẫn đúng.
- Khi dừng. Vòng lặp dừng khi i < n sai, tức i ≥ n. Cùng với i ≤ n trong bất biến, suy ra i = n. Thay vào: s = n(n + 1)/2. Đúng đặc tả.
- Có dừng. Mỗi lượt, đại lượng n − i giảm đúng 1 và không âm, nên vòng lặp phải dừng.
Chứng minh này phủ mọi n, không cần thử. Dù vậy, thử lại với n = 4 cho yên tâm: các lượt cho (i, s) = (1, 1), (2, 3), (3, 6), (4, 10); và 4·5/2 = 10. Khớp.
Chứng minh bắt lỗi ra sao.
Giả sử lập trình viên lỡ viết while (i <= n). Thử chứng minh lại: bước 2 cần "i ≤ n" để suy ra i mới ≤ n, nhưng điều kiện lặp giờ là i ≤ n, nên i mới có thể bằng n + 1 — bất biến gãy. Đúng thế: với n = 4 chương trình chạy thêm một lượt, ra s = 15 thay vì 10. Chỗ chứng minh không đi tiếp được chính là chỗ có lỗi.
Ví dụ 2: máy tìm ra lỗi mà kiểm thử dễ bỏ sót
Hai chương trình A và B dùng chung một máy in, quy ước bằng hai lá cờ. Mỗi bên làm bốn bước:
- Đợi cho tới khi cờ của bên kia hạ.
- Giơ cờ của mình.
- In.
- In xong, hạ cờ.
Tính chất cần đảm bảo: không bao giờ cả hai cùng in. Chạy thử trăm lần có thể đều ổn, vì thường một bên làm xong bước 1–2 trước khi bên kia bắt đầu. Một bộ kiểm tra mô hình thì duyệt mọi cách xen kẽ các bước, và trả về phản ví dụ:
| Bước | Ai làm gì | Cờ A | Cờ B |
|---|---|---|---|
| 1 | A ở bước 1: thấy cờ B hạ, đi tiếp | hạ | hạ |
| 2 | B ở bước 1: thấy cờ A hạ, đi tiếp | hạ | hạ |
| 3 | A giơ cờ | giơ | hạ |
| 4 | B giơ cờ | giơ | giơ |
| 5 | A in; B in — vi phạm | giơ | giơ |
Lỗi nằm ở khoảng hở giữa "nhìn" và "giơ cờ": cả hai cùng nhìn trước khi ai kịp giơ. Đổi thứ tự (giơ cờ trước rồi mới nhìn) thì hết lỗi này nhưng lại sinh ra tình huống cả hai cùng giơ, cùng chờ nhau mãi. Những thuật toán đúng cho bài toán này (như thuật toán Peterson) cần thêm một biến "nhường lượt" — và chính các bộ kiểm tra mô hình được dùng để xác nhận chúng đúng trên mọi cách xen kẽ.
Dòng thời gian
| Năm | Mốc |
|---|---|
| 1969 | Tony Hoare công bố nền tảng tiên đề cho việc chứng minh chương trình (bộ ba Hoare). |
| 1981–1982 | Edmund Clarke và E. Allen Emerson, và độc lập là Jean-Pierre Queille và Joseph Sifakis, đề xuất kiểm tra mô hình. Ba người Clarke, Emerson, Sifakis nhận giải Turing năm 2007. |
| 1994 | Lỗi phép chia của Pentium bị phát hiện. |
| 1996 | Tên lửa Ariane 5 chuyến bay đầu tiên bị phá huỷ chưa đầy một phút sau khi phóng do phần mềm đổi một số thực 64 bit sang số nguyên 16 bit bị tràn — một lỗi mà phân tích hình thức có thể bắt được. |
| 2009 | Nhân hệ điều hành seL4 được công bố là đã chứng minh hình thức đúng đặc tả ở mức mã nguồn. |
| Thập niên 2000–2010 | Trình biên dịch C CompCert được chứng minh đúng bằng bộ chứng minh Coq; các công ty điện toán đám mây dùng ngôn ngữ đặc tả TLA+ của Leslie Lamport để kiểm thiết kế hệ thống phân tán. |
Giới hạn: chứng minh đúng với cái gì?
- Chỉ đúng với đặc tả. Nếu đặc tả viết sai ý người dùng, chương trình "đúng đặc tả" vẫn sai ý. Kiểm chứng chuyển câu hỏi "mã có đúng không" thành "đặc tả có đúng không" — câu sau ngắn hơn, dễ soát hơn, nhưng vẫn phải soát.
- Chỉ đúng với mô hình. Mô hình bỏ qua những gì nằm ngoài nó (nhiễu điện, phần cứng hỏng, thư viện chưa kiểm).
- Không có máy kiểm vạn năng. Theo kết quả của Turing về bài toán dừng, không có thuật toán nào tự động quyết định được mọi tính chất của mọi chương trình. Vì thế kiểm chứng hình thức luôn cần giới hạn phạm vi hoặc cần người dẫn dắt chứng minh.
- Tốn kém. Thường chỉ dùng cho phần cốt lõi, nơi lỗi gây hậu quả lớn: khối số học, nhân hệ điều hành, phần mềm hàng không, y tế, đường sắt, giao thức bảo mật.
Bài tập
- Kiểm thử 1.000 đầu vào đều đúng. Có kết luận được chương trình đúng với mọi đầu vào không? — Đáp án: không; đó là quy nạp không hoàn toàn, chỉ một phản ví dụ chưa thử là đủ bác bỏ.
- Với vòng lặp tính tổng trong bài, khi i = 3 thì s bằng bao nhiêu theo bất biến? — Đáp án: s = 3·4/2 = 6.
- Vì sao cần thêm "i ≤ n" vào bất biến, không chỉ "s = i(i + 1)/2"? — Đáp án: để khi vòng lặp dừng (i ≥ n) suy ra được i = n; thiếu nó chỉ biết i ≥ n.
- Bộ kiểm tra mô hình trả về một chuỗi bước dẫn tới vi phạm. Chuỗi đó gọi là gì trong logic? — Đáp án: phản ví dụ của tính chất "luôn luôn…".
Dùng vào đâu
- Lập trình viên: ngay cả khi không dùng công cụ, tập viết bất biến vòng lặp và điều kiện trước – sau cho hàm giúp bắt lỗi lệch một (off-by-one) trước khi chạy. Nhiều ngôn ngữ có lệnh assert để ghi các điều kiện đó vào mã.
- Sinh viên công nghệ thông tin: môn Phương pháp hình thức, Kiểm thử và đảm bảo chất lượng phần mềm; công cụ đáng thử là TLA+, các bộ kiểm tra mô hình và bộ chứng minh mã nguồn mở.
- Người học logic: đây là nơi phân biệt "hợp lệ" và "đúng" có giá trị bằng tiền thật — chứng minh hợp lệ nhưng tiền đề (đặc tả) sai thì sản phẩm vẫn hỏng.
Câu hỏi thường gặp
Kiểm chứng hình thức là gì?
Là dùng phương pháp logic và toán học để chứng minh một hệ thống phần cứng hoặc phần mềm đúng với đặc tả trên mọi đầu vào và mọi trạng thái. Hai cách làm chính là kiểm tra mô hình (máy duyệt hết trạng thái) và chứng minh định lý (viết chứng minh có máy kiểm).
Kiểm chứng hình thức khác kiểm thử phần mềm thế nào?
Kiểm thử chạy chương trình với một số đầu vào chọn trước, chỉ phát hiện lỗi ở những chỗ đã thử. Kiểm chứng hình thức chứng minh tính đúng cho mọi trường hợp, nhưng tốn công hơn và chỉ đảm bảo đúng so với đặc tả đã viết.
Lỗi FDIV của Pentium là gì?
Là lỗi trong bộ chia số thực của chip Intel Pentium, được giáo sư toán Thomas Nicely phát hiện năm 1994. Vài ô trong bảng tra của thuật toán chia bị thiếu giá trị đúng, khiến một số phép chia sai từ khoảng chữ số thứ năm; Intel ghi nhận chi phí 475 triệu đô-la để thay chip.
Bất biến vòng lặp là gì?
Là một điều kiện đúng trước khi vòng lặp bắt đầu và vẫn đúng sau mỗi lượt lặp. Kết hợp bất biến với điều kiện dừng sẽ suy ra kết quả cuối cùng của vòng lặp, nhờ đó chứng minh được vòng lặp đúng cho mọi đầu vào.
Đã kiểm chứng hình thức thì chương trình có chắc chắn không còn lỗi không?
Không tuyệt đối. Chương trình chỉ được chứng minh đúng với đặc tả và mô hình đã dùng; nếu đặc tả sai ý người dùng hoặc mô hình bỏ sót yếu tố thực tế thì vẫn có thể có lỗi. Dù vậy, nó loại bỏ được cả những lỗi mà kiểm thử gần như không bao giờ chạm tới.
