Il problema: un aggiornamento non è ancora un modello utilizzabile
Un sensore industriale legge temperatura e vibrazioni, poi usa un piccolo modello di intelligenza artificiale per classificare lo stato della macchina. Arriva una nuova versione dei pesi, cioè dei numeri appresi durante l’addestramento. Mentre il dispositivo li salva, qualcuno scollega l’alimentazione. Al ritorno della corrente, il sensore deve scegliere che cosa caricare. Il problema non è soltanto completare il trasferimento: è evitare che una copia incompleta venga scambiata per un modello pronto e che, nel frattempo, sia stata distrutta l’unica copia funzionante.
La domanda dell’articolo è concreta: possiamo organizzare l’aggiornamento in modo che ogni riavvio trovi la vecchia versione integra oppure la nuova versione integra? Costruiremo una macchina a stati, ossia una descrizione delle operazioni e degli stati persistenti che esse lasciano. Ne eseguiremo tutti i punti di interruzione previsti, confrontando la sovrascrittura diretta con due aree separate e un atto finale di attivazione. Il risultato sarà una proprietà condizionata da ipotesi esplicite, non una misura di affidabilità di una scheda commerciale.
Prima dei dettagli: tre significati diversi di «pronto»
Ricevuto significa che il trasferimento ha consegnato dei dati. Verificato significa che quei dati soddisfano controlli definiti: per esempio dimensione attesa, impronta crittografica e compatibilità con il programma che esegue il modello. Attivo significa che la procedura di avvio è autorizzata a selezionarli. Questi tre eventi non devono coincidere. Una notifica di download completato non prova che i dati siano già persistenti; una verifica positiva non obbliga ad attivare immediatamente il candidato. Separare gli eventi rende possibile ragionare su cosa accade fra uno e l’altro.
Nel nostro scenario il programma di inferenza, chiamato runtime, rimane installato: aggiorniamo i pesi trattandoli come dati. La memoria flash conserva informazioni senza alimentazione; la RAM normalmente no. Chiameremo slot una regione di memoria riservata a una copia. Il registro delle attivazioni, o journal, conserva piccole descrizioni delle copie selezionabili. È utile immaginarlo come un indice delle edizioni disponibili di un libro, ma l’analogia finisce qui: una memoria reale impone blocchi di cancellazione, vincoli di programmazione e possibili scritture interrotte che un indice cartaceo non rappresenta.
Il contratto che rende possibile il ragionamento
Assumiamo scritture persistenti e ordinate: se il programma completa un passo prima di iniziare il successivo, dopo il riavvio ritroviamo quel passo. Assumiamo inoltre un marcatore finale atomico: al riavvio appare non impostato oppure impostato, mai in uno stato ambiguo accettato per errore. I due slot sono indipendenti, la vecchia copia confermata rimane integra, e metadati e impronta attesa provengono da una fonte fidata. Il contatore delle generazioni cresce senza traboccare. Sono precondizioni del modello matematico; un progetto hardware deve dimostrare come realizzarle o modificare il protocollo quando non valgono.
Introduciamo l’interruzione solo fra operazioni astratte completate. Non simuliamo il circuito della flash mentre perde tensione, una scrittura spezzata a metà, una cache non scaricata o il danneggiamento di un settore vicino. Questa distinzione è decisiva: enumerare tutti gli stati del nostro programma Python non significa aver provato tutti i guasti di un microcontrollore. Il piccolo esperimento risponde a una domanda logica sul protocollo. Le prove elettriche, temporali e di durata della memoria restano un secondo livello di verifica, necessario prima di utilizzare il disegno su un dispositivo.
Il caso minimo: quattro parti e una sola copia
Riduciamo il vecchio modello a quattro byte [1, 1, 1, 1] e quello nuovo a [2, 2, 2, 2]. Non sono pesi utili per inferenza: rappresentano quattro parti di un file, rendendo visibile quando una copia è completa. Il programma ingenuo cancella lo slot e poi scrive una parte alla volta. Ha cinque operazioni e sei punti osservabili di interruzione, compreso quello precedente alla prima operazione. Prima di cancellare esiste il vecchio modello; dopo tutte le scritture esiste quello nuovo. Nei quattro punti intermedi non esiste nessuna delle due copie integre.
La sequenza [2, 2, vuoto, vuoto] non diventa un modello corretto perché il trasferimento riprenderà in seguito. Al momento del riavvio manca già il materiale necessario. Possiamo decidere di fermare l’inferenza e attendere un recupero, scelta talvolta accettabile; non possiamo dichiarare continuità operativa. Neppure scrivere prima un’etichetta «versione 2» risolve il problema: un’etichetta non completa i dati. Se viene interpretata come autorizzazione al caricamento, anticiparla rende anzi più facile selezionare una copia parziale. La proprietà utile riguarda dati e procedura di selezione insieme.
Due copie e una decisione presa alla fine
Conserviamo la copia confermata nello slot A e prepariamo il candidato nello slot B. Le otto operazioni sono: cancellare B, scrivere le sue quattro parti, verificarne l’impronta, aggiungere al journal un record ancora non attivo, impostare il marcatore di commit. Commit significa rendere la decisione osservabile al riavvio. Il record contiene la generazione, il nome dello slot, la versione di runtime richiesta e l’impronta attesa. Il numero di generazione ordina le attivazioni: non misura la qualità del modello e non deve essere confuso con una valutazione scientifica delle sue prestazioni.
Al riavvio leggiamo i record dal più recente al più vecchio. Accettiamo il primo che sia attivo, compatibile e associato a dati completi con l’impronta corretta. La verifica viene ripetuta sui dati effettivamente presenti: non basta ricordare che il download era stato controllato prima dell’interruzione. Se il candidato non supera i controlli, proviamo il record precedente. Se nessuno li supera, il risultato è «nessun modello valido». Questa risposta esplicita evita che la procedura trasformi l’assenza di una copia utilizzabile in un caricamento arbitrario e apparentemente riuscito.
La formula risponde alla domanda «quali copie possono essere scelte?». La lettera r indica un record; AND richiede che tutte le condizioni siano vere. complete verifica che non manchino parti, mentre hash_ok confronta l’impronta calcolata con quella attesa. Nel codice i due controlli sono raccolti nella funzione valid. Non ci sono unità fisiche in questa espressione: sono predicati logici. Per esempio, un record con commit vero ma runtime richiesto 2 non è selezionabile se il dispositivo esegue runtime 1, anche quando tutti i byte coincidono con quelli ricevuti.
Che cosa mostra davvero l’esperimento
La figura raccoglie l’esecuzione dei due programmi. Ogni punto è un riavvio dopo un certo numero di operazioni completate. Nel pannello superiore i punti rossi indicano una copia inutilizzabile; in quello inferiore la versione precedente rimane selezionata fino al commit finale. Le scale orizzontali contano operazioni differenti nei due protocolli, non secondi: il punto 5 del primo pannello non corrisponde allo stesso istante del punto 5 del secondo. Il confronto riguarda gli esiti possibili della selezione, non la velocità di aggiornamento.
| Protocollo | Punti esaminati | Vecchio | Nuovo | Nessuno valido |
|---|---|---|---|---|
| A: overwrite | 6 | 1 | 1 | 4 |
| B: dual + commit | 9 | 8 | 1 | 0 |
Quattro punti problematici su sei non significano una probabilità di guasto del 66,7%. Non abbiamo assegnato una distribuzione temporale alle interruzioni, misurato la durata delle operazioni o modellato la tensione di alimentazione. Cancellare un blocco e scrivere un byte non richiedono necessariamente lo stesso tempo. Analogamente, zero stati invalidi sui nove esaminati non è una stima statistica di rischio zero. È una verifica esaustiva dei soli punti di taglio ammessi dalla nostra astrazione. Confondere queste due letture trasformerebbe un risultato logico utile in una promessa di affidabilità non sostenuta dai dati.
La ragione del risultato: preservare un invariante
Un invariante è una proprietà che resta vera dopo ogni passo ammesso. Qui la proprietà è: prima del commit esiste almeno una copia selezionabile, ed è A. All’inizio è vera per costruzione. Cancellare e scrivere B non cambia A, perché gli slot sono indipendenti. Verificare B non cambia A. Aggiungere un record non attivo non rende B selezionabile. Abbiamo così una dimostrazione per induzione sui passi: se la proprietà vale prima di ciascuna operazione precedente al commit, vale anche dopo. Un riavvio in uno di questi punti torna ad A.
Quando il marcatore atomico diventa attivo, B è già completo e verificato; il suo record più recente lo rende preferibile. Se il controllo al riavvio rileva invece un candidato inutilizzabile, A rimane disponibile. L’ordine è essenziale: rendere attivo il record prima di completare i dati distrugge il ragionamento. Anche l’indipendenza è essenziale: se cancellare B cancella fisicamente parte di A perché le due regioni condividono un settore, l’invariante non vale più. Non basta disegnare due rettangoli nella mappa della memoria; bisogna rispettare la granularità reale delle operazioni distruttive.
Tre prove negative, compresa quella che deve fallire
Il programma esegue anche tre casi separati dall’interruzione. Corrompe un byte del candidato già attivo: l’impronta non coincide e riparte A. Cambia nel record del candidato il runtime richiesto da 1 a 2: il contenuto è integro ma incompatibile e riparte A. Infine corrompe B e cancella A: la selezione restituisce None, cioè nessuna copia utilizzabile. Quest’ultimo test è importante quanto i primi due. Mostra il confine della proprietà: due slot non proteggono dalla perdita contemporanea di entrambe le copie e la procedura non deve nascondere questa condizione.
L’impronta usata è SHA-256, una funzione che riassume i byte in una sequenza di lunghezza fissa. Nel nostro esempio rileva la modifica intenzionale del dato di prova, ma non dimostra da chi provenga il modello. Se un avversario può sostituire insieme file e impronta attesa, il confronto può riuscire anche per un file non autorizzato. Autenticità del pacchetto, protezione delle chiavi, verifica delle firme e autorizzazione degli aggiornamenti richiedono un disegno distinto. Qui assumiamo metadati fidati e non eseguiamo una valutazione di sicurezza del canale di distribuzione.
Quanto spazio costa conservare la via di ritorno?
Passiamo dai quattro byte didattici a un dimensionamento ipotetico, senza attribuirlo a una scheda. Un modello occupa W = 1.048.576 byte, cioè 1 MiB; ogni copia ha H = 256 byte di intestazione. La cancellazione avviene su blocchi di E = 4.096 byte, e riserviamo J = 8.192 byte al journal. Per impedire che una cancellazione attraversi il confine fra copie, arrotondiamo ogni slot al multiplo successivo di E. La formula seguente risponde quindi a una domanda fisica precisa: quanti byte di flash riservare a questo schema?
S è la dimensione riservata a uno slot e F quella totale; ceil significa arrotondamento all’intero superiore. KiB vale 1.024 byte e MiB vale 1.048.576 byte. Il calcolo eseguito restituisce 2.113.536 byte: già 16.384 byte oltre una memoria da 2 MiB, prima di aggiungere runtime, avvio e altri dati. Dire «il modello pesa un megabyte, quindi due megabyte bastano» sarebbe sbagliato anche in questo esempio minimo. Il totale riguarda memoria persistente, non il picco di RAM necessario all’inferenza, che dipende anche da attivazioni, buffer e implementazione degli operatori.
Integrità non significa compatibilità completa, né qualità
Il nostro controllo di compatibilità usa un solo intero per il runtime: è intenzionalmente elementare. In un’applicazione AI, lo stesso file di pesi può richiedere forma degli ingressi, ordine dei canali, unità dei sensori, normalizzazione, operatori e mappa delle etichette specifici. Cambiare la normalizzazione lasciando vecchi pesi può produrre un sistema che si avvia regolarmente e decide male. Il manifesto del pacchetto dovrebbe identificare l’insieme coerente di queste dipendenze. Ripristinare i soli pesi non è un rollback completo se il resto della configurazione è già cambiato in modo incompatibile.
Il commit del nostro programma rende B selezionabile; non implementa un periodo di prova con conferma successiva. Un’estensione pratica potrebbe distinguere candidato, avvio di prova e versione confermata, usando un controllo di funzionamento e un limite ai tentativi. Bisognerebbe allora definire anche che cosa succede se manca corrente durante la conferma. Inoltre superare un test di avvio non prova che il modello sia accurato su dati futuri. Continuità dell’avvio, correttezza dell’interfaccia e validità predittiva sono tre proprietà diverse: nessuna può essere dedotta automaticamente dalle altre due.
Confronto con sistemi reali e alternative
La documentazione ufficiale di MCUboot descrive aggiornamenti di immagini firmware con modalità di prova, conferma e ritorno, oltre a informazioni persistenti per recuperare scambi interrotti. È un riferimento pertinente per capire la distanza fra una regola astratta e un bootloader configurabile. Il nostro codice non esegue MCUboot, non ne riproduce l’algoritmo e non aggiorna firmware.
Le alternative dipendono dal vincolo dominante. Un solo slot con ripristino via rete risparmia spazio locale ma accetta un intervallo senza inferenza e dipende dalla disponibilità del recupero. Due slot conservano una copia pronta, al prezzo della memoria aggiuntiva. Un aggiornamento differenziale trasferisce soltanto differenze, ma ridurre i byte trasmessi non garantisce che l’applicazione della modifica sia interrompibile senza danni: serve ancora una strategia per preservare lo stato precedente. Un file temporaneo seguito da sostituzione del nome sposta parte del problema sul contratto del filesystem, compresa la persistenza dell’operazione dopo perdita di alimentazione.
Anche il journal va progettato per durare. Nel codice è una lista Python ordinata a ogni avvio e il contatore non trabocca. Una memoria reale è finita: eliminare record vecchi, riciclare settori e gestire l’usura introducono altre transizioni da analizzare. Con R record, l’ordinamento didattico costa O(R log R); verificare una copia di W byte richiede O(W) lavoro di hashing e, nel caso di ripiego su A, può richiedere la lettura di due copie. Queste complessità non forniscono millisecondi o millijoule: servono misure della piattaforma per trasformarle in latenza ed energia.
Come riprodurre e che cosa verificare sul dispositivo
L’archivio allegato contiene experiment.py, plot.py, risultati JSON e istruzioni nelle quattro lingue. L’esperimento è deterministico, quindi non usa un seme casuale. Eseguendo experiment.py si enumerano gli stati e si controllano automaticamente le proprietà dichiarate; plot.py disegna gli esiti, non misura hardware. Il breve codice in fondo richiama lo stesso calcolo, stampa le coppie punto/esito, i tre casi negativi e il totale dei byte. La riga che decide davvero il caricamento, nel file completo, accetta un record solo dopo commit, compatibilità e verifica della copia: è lì che la spiegazione diventa una regola eseguibile.
Su hardware proporremmo invece interruzioni controllate durante cancellazione, programmazione, aggiornamento dei metadati e conferma; non soltanto fra funzioni software. Andrebbero specificati scheda, flash, versioni, configurazione, tensioni e protocollo, verificando anche candidato corrotto, dipendenze errate, perdita del journal e fallimento dell’avvio di prova. Questo è un piano di verifica non eseguito. Non disponiamo qui di misure di tempo di riavvio, energia, usura o probabilità di guasto. Neppure attribuiamo questo esperimento a un prodotto embedded EL-AI: è un’analisi didattica del problema, non la documentazione di un’installazione aziendale.
La risposta: proteggere la copia prima di scegliere la nuova
Se manca corrente, nel nostro protocollo riparte A fino al commit e riparte B dopo il commit, purché il candidato superi i controlli; altrimenti si torna ad A se ancora valida. La ragione non è una particolare capacità dell’intelligenza artificiale: è aver conservato una copia integra e rimandato la decisione di usarne un’altra fino a quando i dati sono pronti. Questo risultato chiarisce cosa chiedere a un aggiornamento embedded: una regola di selezione verificabile, uno stato precedente preservato e ipotesi realizzabili sulla memoria. La simulazione dimostra il ragionamento sotto quelle ipotesi; il dispositivo deve ancora dimostrare di rispettarle.
Fonte tecnica e materiale riproducibile
from experiment import run
r = run()
for name in ['naive', 'dual']:
print(name, [(x['cut'], x['outcome']) for x in r[name]])
print(r['negative_cases'])
print(r['memory']['total_flash_bytes'])Codice, dati e istruzioni · JSON. Calcoli didattici eseguiti con Python 3.14.0; figure con Matplotlib 3.11.2. Analisi con assistenza AI, senza dichiarare peer review o revisione umana. Copertina originale ImageGen, illustrativa: non documenta persone, sedi o installazioni EL-AI. Fonti consultate il 6 ottobre 2026.