Kekerasan komputasi dari program komputer "nyata"

Saya sering mendengar dikatakan bahwa Anda tidak dapat menulis sebuah program untuk menangkap bug di browser web, atau pengolah kata, atau sistem operasi, karena Teorema Rice: properti semantik apa pun untuk bahasa lengkap Turing tidak dapat diputuskan.

Namun, saya tidak yakin sejauh mana ini berlaku untuk program dunia nyata suka sistem operasi. Apakah jenis program ini membutuhkan kekuatan penuh dari kelengkapan Turing? Apakah ada model perhitungan yang lebih sederhana (seperti PR) di mana aplikasi ini dapat ditulis? Jika demikian, sejauh mana hal ini memungkinkan kesesuaian kebenaran program?

Anda tentu dapat menulis program yang menangkap bug - ada komunitas besar dan aktif orang yang menulis program untuk melakukan hal itu. Namun, teorema Rice mencegah Anda dari melakukan adalah menulis bug-catcher yang baik dan lengkap (yaitu, menangkap semua bug dari kelas tertentu tanpa positif palsu).

Yang mengatakan, pembatasan naif pada model perhitungan sebenarnya tidak banyak membantu Anda dalam meningkatkan kepraktisan analisis program. Alasannya adalah bahwa Anda bisa mendapatkan program yang melakukan "hal yang hampir sama" dengan memutar sambil memutar

while P do 
   C

menjadi for-loop dengan konstanta iterasi besar:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Sekarang program ini bahkan tidak memerlukan kekuatan penuh dari rekursif primitif (karena for-loop dapat diperluas secara makro menjadi pernyataan bersarang jika-maka-yang lain), tetapi dalam kebanyakan kasus praktis ia akan berperilaku sama seperti sebelumnya. Perhatikan bahwa hal ini membantu decidability dalam teori - program ini total, sehingga Anda dapat menjawab pertanyaan dengan menjalankan program dan melihat apa yang terjadi. Ini bukan yang sebenarnya kita inginkan, yaitu untuk mendapatkan jawaban lebih cepat daripada menjalankan program - penghentian buatan yang diperkenalkan sebenarnya tidak membantu analisis program dalam praktik, karena bug terjadi karena kesalahan dalam logika program nyata, dan kami belum Aku tidak menyentuh itu sama sekali.

$\epsilon_0$

Karena Anda bertanya tentang kebenaran program dari program dunia nyata seperti sistem operasi, Anda mungkin tertarik dengan proyek seL4 ( jurnal , pdf , konferensi ).

Tim NICTA mengambil microkernel generasi ketiga dari 8700 baris C dan 600 baris assembler diimplementasikan sesuai dengan spesifikasi abstrak di Haskell. Mereka memberikan bukti formal yang diperiksa mesin (dalam Isabelle / HOL) bahwa implementasinya secara ketat mengikuti spesifikasi. Dengan demikian membuktikan bahwa program mereka bebas bug.

Jadi sama seperti masalah penghentian, meskipun tidak dapat dipecahkan secara umum, ini dapat diselesaikan untuk beberapa kasus tertentu. Dalam hal ini, walaupun Anda tidak dapat membuktikan bahwa kode C yang arbitrer bebas bug, mereka dapat melakukannya dalam kasus seL4 microkernel.

Pertanyaan yang Anda ajukan sebenarnya sangat berbeda.

Namun, saya tidak yakin sejauh mana ini berlaku untuk program dunia nyata suka sistem operasi. Apakah jenis program ini membutuhkan kekuatan penuh dari kelengkapan Turing?

Dibutuhkan sangat sedikit untuk model komputasi untuk menjadi Turing lengkap. Misalnya, berbagai model dengan penghitung dapat mensimulasikan mesin Turing. Jika Anda yakin perangkat lunak Anda membutuhkan lebih dari dua penghitung yang dapat Anda manipulasi secara sewenang-wenang, Anda menggunakan bahasa lengkap Turing. Meskipun bilangan bulat mesin dibatasi apriori, struktur data yang dialokasikan heap biasanya tidak. Jika perangkat lunak Anda membutuhkan daftar, pohon, dan data yang dialokasikan secara dinamis lainnya, Anda menggunakan bahasa lengkap Turing.

Apakah ada model perhitungan yang lebih sederhana (seperti PR) di mana aplikasi ini dapat ditulis? Jika demikian, sejauh mana hal ini memungkinkan kesesuaian kebenaran program?

Penting untuk mengetahui bahwa kami tidak ingin memeriksa properti sewenang-wenang dari perangkat lunak kami. Memeriksa properti yang sangat spesifik dan sempit (tidak ada buffer overflows, tidak ada null-pointer dereferences, tidak ada loop tak terbatas, dll) sangat meningkatkan kualitas dan kegunaan perangkat lunak. Secara teori, masalah seperti itu masih belum dapat dipastikan. Dalam praktiknya, fokus pada properti tertentu memungkinkan kita menemukan struktur dalam program kita yang sering kita manfaatkan untuk menyelesaikan masalah.

Secara khusus, Anda dapat memodifikasi pertanyaan awal Anda

Apakah ada abstraksi perangkat lunak saya yang dapat saya analisis secara efisien dalam model lengkap non-Turing?

Abstraksi adalah model yang mencakup perilaku perangkat lunak asli dan mungkin banyak perilaku tambahan. Ada model seperti mesin satu-counter atau sistem pushdown yang Turing tidak lengkap dan yang bisa kita analisis. Pendekatan standar dalam verifikasi program dengan alat otomatis adalah dengan membangun abstraksi dalam model seperti itu dan memeriksanya secara algoritmik.

Ada aplikasi di mana orang-orang peduli dengan properti canggih dari perangkat keras atau perangkat lunak mereka. Perusahaan perangkat keras ingin agar chip mereka menerapkan algoritma aritmatika dengan benar, perusahaan otomotif dan avionik menginginkan perangkat lunak yang benar secara sertifikasi. Jika itu penting, Anda lebih baik menggunakan manusia (terlatih).