Η είδηση έσκασε πρόσφατα έχει γίνει πρόταση για ένταξη ο πυρήνας του Linux 5.20 (ή ίσως το υποκατάστημα θα έχει τον αριθμό 6.0, όλα εξαρτώνται από την απόφαση του Linus Torvalds λόγω του σχολίου που έκανε στην κυκλοφορία του Kernel 5.19).
Η πρόταση που έγινε αφορά ένα σύνολο μπαλωμάτων με την εφαρμογή του μηχανισμού RV (Επαλήθευση χρόνου εκτέλεσης), που είναι ένα μέσο επαλήθευσης της σωστής λειτουργίας σε συστήματα υψηλής αξιοπιστίας που εγγυώνται την απουσία αστοχιών.
επικύρωση γίνεται κατά τη διάρκεια της εκτέλεσης με την προσάρτηση χειριστών σε σημεία παρακολούθησης που ελέγχουν την πραγματική πρόοδο της εκτέλεσης σε σχέση με ένα προκαθορισμένο ντετερμινιστικό μοντέλο αναφοράς του αυτόματου που καθορίζει την αναμενόμενη συμπεριφορά του συστήματος.
Προγραμματιστής Linux, Ο Daniel Bristot de Oliveira αναφέρει:
Τα τελευταία χρόνια, διερευνώ τη δυνατότητα επαλήθευσης της συμπεριφοράς του πυρήνα Linux χρησιμοποιώντας την Επαλήθευση χρόνου εκτέλεσης.
Η επαλήθευση χρόνου εκτέλεσης (RV) είναι μια ελαφριά (αλλά αυστηρή) μέθοδος που συμπληρώνει τις κλασικές εξαντλητικές τεχνικές επαλήθευσης (όπως ο έλεγχος μοντέλων και η απόδειξη θεωρημάτων) με μια πιο πρακτική προσέγγιση σε πολύπλοκα συστήματα. Αντί να βασίζεται σε ένα λεπτομερές μοντέλο ενός συστήματος (για παράδειγμα, μια επανεφαρμογή ενός επιπέδου εντολών), το VR λειτουργεί αναλύοντας το πραγματικό ίχνος εκτέλεσης του συστήματος, συγκρίνοντάς το με μια επίσημη προδιαγραφή της συμπεριφοράς του συστήματος.
Η χρήση ντετερμινιστικών αυτόματα για VR είναι μια καθιερωμένη προσέγγιση. Για τη συγκεκριμένη περίπτωση του πυρήνα Linux, μπορείτε να μάθετε πώς να μοντελοποιείτε τη σύνθετη συμπεριφορά του πυρήνα Linux με αυτό το άρθρο:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; Ντε Ολιβέιρα, Ρομούλο Σίλβα. *Αποτελεσματική επίσημη επαλήθευση για τον πυρήνα Linux.* Στο: Διεθνές Συνέδριο για την Μηχανική Λογισμικού και τις Επίσημες Μέθοδοι. Springer, Cham, 2019. Σελ. 315-332.
Και πόσο αποτελεσματική είναι αυτή η προσέγγιση εδώ:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Ένα μοντέλο συγχρονισμού νημάτων για τον πυρήνα Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Η σύνθετη συμπεριφορά μπορεί να μοντελοποιηθεί με αρθρωτό τρόπο, με αποδεκτά γενικά έξοδα (ακόμη και για συστήματα παραγωγής).
Αναφέρεται ότι Οι πληροφορίες σημείου παρακολούθησης μετακινούν το μοντέλο από τη μια κατάσταση στην άλλη, και εάν η νέα κατάσταση δεν ταιριάζει με τις παραμέτρους του μοντέλου, δημιουργείται μια προειδοποίηση ή ο πυρήνας εισέρχεται σε κατάσταση "πανικού" (υποθέτοντας ότι τα εξαιρετικά αξιόπιστα συστήματα θα εντοπίσουν και θα ανταποκριθούν σε τέτοιες καταστάσεις).
Το μοντέλο του αυτόματου ορίζει μεταβάσεις από τη μια κατάσταση στην άλλη εξάγονται σε μορφή "dot". (graphviz), μετά το οποίο μεταφράζεται χρησιμοποιώντας το βοηθητικό πρόγραμμα dot2c σε μια αναπαράσταση C, η οποία φορτώνεται με τη μορφή μιας μονάδας πυρήνα που παρακολουθεί τις αποκλίσεις. εκτέλεση από ένα προκαθορισμένο μοντέλο.
Ο έλεγχος των μοντέλων κατά το χρόνο εκτέλεσης τοποθετείται ως πιο ελαφριά και ευκολότερη μέθοδος να εφαρμόσει για την επαλήθευση της ορθότητας της εκτέλεσης σε κρίσιμα για την αποστολή συστήματα, το οποίο συμπληρώνει τις κλασικές μεθόδους επαλήθευσης της αξιοπιστίας, όπως η επαλήθευση μοντέλου και οι μαθηματικές αποδείξεις της συμμόρφωσης του κώδικα με τις προδιαγραφές που δίνονται σε επίσημη γλώσσα.
Ο συντηρητής του υποσυστήματος παρακολούθησης Steven Rostedt το συνόψισε ως εξής:
» Αυτή είναι η μεγαλύτερη αλλαγή για αυτό το αίτημα έλξης. Παρουσιάζει την επαλήθευση χρόνου εκτέλεσης που απαιτείται για την εκτέλεση του Linux σε κρίσιμα για την ασφάλεια συστήματα. Επιτρέπει την εισαγωγή ντετερμινιστικών μοντέλων αυτόματα στον πυρήνα που θα προσαρτηθούν σε σημεία παρακολούθησης, όπου οι πληροφορίες σχετικά με αυτά τα σημεία παρακολούθησης θα μετακινήσουν το μοντέλο από τη μια κατάσταση στην άλλη.
Μεταξύ των αναφερθέντων πλεονεκτημάτων του RV είναι η ικανότητα παροχής αυστηρής επαλήθευσης χωρίς χωριστή υλοποίηση ολόκληρου του συστήματος σε μια γλώσσα μοντελοποίησης, καθώς και μια ευέλικτη απόκριση σε απρόβλεπτα γεγονότα, για παράδειγμα, να εμποδίζει τη διάδοση της αστοχίας κρίσιμων συστημάτων.
Τέλος, εάν ενδιαφέρεστε να μάθετε περισσότερα για αυτό, μπορείτε να συμβουλευτείτε τις λεπτομέρειες στο παρακάτω σύνδεσμο.
πηγή: https://www.phoronix.com/