Aspettare venti tick sembra facile, finché il numero torna piccolo
Un dispositivo embedded acquisisce un dato, avvia un’inferenza AI e attende il risultato entro un certo intervallo. Il firmware legge un contatore crescente: basta salvare la scadenza e confrontarla con il valore corrente? Vicino al limite del contatore, quel confronto può dichiarare un timeout appena iniziata l’attesa. Il problema non è la velocità del modello: è il modo in cui rappresentiamo il tempo con un numero finito di bit.
Studieremo un contatore senza segno di 16 bit, cioè con valori da 0 a 65535. Partiremo da 65530 e aspetteremo 20 incrementi. La scadenza rappresentata sarà 14, un numero minore del punto iniziale. Deriveremo perché la differenza modulare recupera correttamente il tempo trascorso in condizioni precise, e perché non può recuperare un intero giro non osservato. Ogni numero proviene da un programma Python eseguito: non abbiamo compilato firmware, misurato una scheda o eseguito un kernel sul dispositivo.
Prima i tick, poi i secondi
Un tick è un incremento discreto del contatore. Assumere 1000 tick al secondo consente di convertire i conteggi in secondi, ma non trasforma il nostro programma in una misura temporale. Il contatore a 16 bit torna al valore iniziale dopo 65536 incrementi, cioè 65,536 s alla frequenza ipotizzata. Il medesimo ragionamento su 32 bit dà circa 49,71 giorni. Aumentare i bit allontana il problema: non rende corretta una relazione d’ordine che non sa attraversare il ritorno a zero.
M è il numero di stati disponibili, non il massimo valore memorizzabile: il massimo è M−1. Il simbolo mod indica il resto nella divisione per M, scelto tra 0 e M−1. Il confronto corrente maggiore o uguale a 14 è già vero quando il contatore vale 65530. Eppure non è passato alcun tick. Sappiamo quindi che quel confronto non può rappresentare da solo l’idea di attesa, anche se funzionerebbe in un esempio lontano dal limite.
Confrontare un intervallo, non due etichette sul quadrante
Il contatore somiglia a un quadrante che dopo l’ultima tacca riparte dalla prima. L’analogia aiuta a vedere perché il numero piccolo non significa necessariamente prima; non garantisce quante rotazioni siano avvenute. Per recuperare la distanza percorsa da un punto iniziale calcoliamo la differenza e riportiamola nello stesso insieme di stati. Questa operazione è una differenza modulare, diversa da una semplice sottrazione tra interi illimitati.
Dopo 11 tick, il contatore vale 5. La sottrazione ordinaria 5−65530 è negativa; riportata modulo 65536 diventa 11. Dopo 20 tick il contatore vale 14 e la differenza modulare vale 20: raggiunge la durata richiesta. Il criterio interpreta correttamente anche i valori immediatamente prima e dopo la scadenza. Prima di chiamarlo una soluzione universale, però, dobbiamo dimostrare quale informazione contiene realmente delta.
La dimostrazione indica anche il limite
Chiamiamo E il vero numero di incrementi trascorsi dall’inizio. È una variabile del nostro modello di riferimento, non un’informazione contenuta automaticamente nel contatore. Se il dispositivo incrementa senza salti o reset, now è il resto di start+E. Sostituendo questa espressione nella differenza modulare, start si cancella: il risultato è E modulo M. Per E compreso tra 0 e M−1, quel resto coincide con E stesso.
Abbiamo dunque una condizione sufficiente precisa: l’intervallo effettivo dall’inizio deve essere inferiore a un giro completo. La soglia duration deve essere rappresentabile e deve descrivere la stessa unità di conteggio. In queste condizioni confrontare delta con duration equivale a confrontare il vero tempo in tick con la soglia. Il metodo non richiede che il valore corrente sia numericamente maggiore di quello iniziale; richiede invece un limite sull’intervallo che quei due valori rappresentano.
| E reale (tick) | now | delta | Scaduto corretto | Test ingenuo |
|---|---|---|---|---|
| 0 | 65530 | 0 | 0 | 1 |
| 5 | 65535 | 5 | 0 | 1 |
| 11 | 5 | 11 | 0 | 0 |
| 19 | 13 | 19 | 0 | 0 |
| 20 | 14 | 20 | 1 | 1 |
| 26 | 20 | 26 | 1 | 1 |
Nella tabella 1 significa vero e 0 falso; il test ingenuo è now maggiore o uguale alla scadenza 14. Le prime due righe sono il fallimento importante: il programma potrebbe interrompere l’inferenza senza aver concesso l’attesa richiesta. Le righe successive mostrano perché un test svolto soltanto dopo il ritorno a zero potrebbe dare l’impressione che il criterio funzioni. Per provare un algoritmo temporale servono anche casi prima della transizione, non solo il numero finale.
Un giro nascosto non si può ricostruire da due letture
Ora lasciamo passare esattamente 65536 tick senza informazioni aggiuntive. Il contatore torna a 65530, il valore iniziale, e delta vale 0. La vera attesa 20 è ampiamente trascorsa, ma il confronto modulare non la riconosce. Non è un difetto della dimostrazione: ne abbiamo violato l’ipotesi E minore di M. Le due osservazioni sono identiche a quelle di un’attesa nulla; nessun algoritmo che riceva soltanto quelle osservazioni può distinguerle con certezza.
La soluzione richiede informazione o vincoli ulteriori: un contatore di epoche, un intervallo massimo garantito tra osservazioni, un timer più largo o un servizio temporale del sistema operativo che gestisca lo stato necessario. Leggere periodicamente non basta come promessa vaga: bisogna collegare la frequenza di controllo al massimo ritardo possibile, compresi sospensione e blocchi. Se il dispositivo si riavvia o il contatore viene azzerato per altre ragioni, non siamo più nel modello di semplice incremento modulare.
Perché si sente parlare anche di mezzo giro
Un problema diverso è decidere quale di due timestamp arbitrari venga prima, senza conoscere già la direzione del tempo tra loro. Su un quadrante di 8 stati,0 e 4 sono opposti: la distanza modulare è 4 in entrambi i versi. Per attribuire un ordine locale bisogna scegliere un orizzonte inferiore a mezzo giro. Questa condizione non va confusa con quella appena dimostrata: recuperare un intervallo non negativo noto come trascorso ammette E inferiore a un giro, mentre ordinare timestamp generici è un’altra domanda.
Non useremo quindi una conversione automatica a intero con segno come scorciatoia universale. Oltre alle ipotesi sul mezzo intervallo, quella tecnica dipende dalle regole del linguaggio e della rappresentazione. Il nostro codice usa esplicitamente il resto modulo M su interi Python, così il modello aritmetico è visibile. Non è una prova di equivalenza con qualsiasi espressione C apparentemente simile, compilata su qualsiasi processore.
Il tipo della variabile non è sempre il tipo della sottrazione
Nel linguaggio C, due operandi piccoli possono subire promozioni intere prima della sottrazione. Per esempio, se un int può rappresentare tutti i valori di un tipo senza segno a 16 bit, gli operandi possono essere promossi a int. La sottrazione 5−65530 viene allora calcolata come un intero negativo rappresentabile, non direttamente come un’operazione modulo 65536. Assegnare il risultato a un tipo senza segno della larghezza voluta introduce poi la conversione modulare. Sono due passaggi distinti.
La distinzione è documentata nel draft pubblico N1570del 12 aprile 2011: sezioni 6.2.5,6.3.1.1 e 6.3.1.3. Lo citiamo come draft C11, non come descrizione certificata di ogni compilatore attuale. Un confronto eseguito prima della conversione può usare un valore diverso da quello previsto dal modello. Non abbiamo compilato né verificato un listato C; chi implementa deve controllare tipi effettivi, promozioni, costanti e conversioni sul proprio toolchain, senza dedurre correttezza dal solo nome di una variabile.
Che cosa fa davvero il kernel: non soltanto una sottrazione
Abbiamo letto il metodo xTaskCheckForTimeOut nel file tasks.c di FreeRTOS-Kernel V11.2.0, una versione esplicita e non un generico riferimento al ramo corrente. Il metodo legge il conteggio in una sezione critica, considera uno stato dei ritorni a zero e aggiorna il tempo rimanente quando l’attesa continua. Gestisce inoltre opzioni come l’interruzione del blocco e l’attesa indefinita. Questo riassunto riguarda il metodo letto; non equivale a eseguire o validare l’intero kernel.
Il caso del giro nascosto non dimostra quindi che FreeRTOS sbagli: il nostro modello riceve due letture e basta, mentre il metodo del kernel dispone di stato aggiuntivo. La lezione è confrontare interfacce con la stessa informazione disponibile. Copiare soltanto una riga di sottrazione da un algoritmo che usa anche epoche, sezioni critiche e aggiornamenti dello stato può eliminare proprio le condizioni che lo rendevano corretto.
La lettura atomica è un problema separato dall’aritmetica. Un contatore largo letto in più operazioni può combinare parti appartenenti a istanti diversi; un reset può cambiare il significato dell’epoca. Qui assumiamo letture coerenti e nessun reset. Il codice Python non prova l’atomicità di una lettura su microcontrollore, né l’efficacia di una sezione critica su una specifica architettura. Servirebbero piattaforma, compilatore, configurazione e prove dedicate.
Il programma controlla una proprietà, non misura una prestazione
Per verificare la derivazione senza affidarci a pochi valori abbiamo ridotto il contatore a 8 bit e provato tutte le 256 posizioni iniziali con tutti i 256 intervalli da 0 a 255. Sono 65536 casi: in ciascuno la differenza modulare coincide con l’intervallo reale. Non è una percentuale di affidabilità né un campionamento statistico. È una verifica esaustiva del modello ridotto e della proprietà specifica; la dimostrazione precedente spiega perché la stessa identità vale per qualunque M sotto le ipotesi dichiarate.
Provare tutte le coppie costa M²casi: con b bit sono 4 alla b. Per questo l’esempio esaustivo usa 8 bit e non afferma di aver esplorato ogni storia di un sistema a 16 o 32 bit. La singola differenza richiede invece un numero costante di operazioni aritmetiche se il contatore entra in una parola macchina. Ciò non è una misura in microsecondi: implementazione, compilatore e piattaforma determinano il costo reale. Gli interi illimitati di Python non sono un modello del consumo energetico di una MCU.
Il frammento allegato separa E, il tempo reale noto alla simulazione, da now, la sola lettura che riceverebbe l’algoritmo. Conservare entrambe le variabili è essenziale per scoprire l’alias temporale: se generassimo il valore atteso usando la stessa differenza modulare, il test ripeterebbe l’implementazione e non controllerebbe il limite del giro intero. I dati salvati comprendono proprio il caso E uguale a M, nel quale il metodo non dispone dell’informazione necessaria.
Dai conteggi a una vera deadline di inferenza
Venti tick non sono automaticamente una garanzia di completamento in 20 millisecondi. Anche assumendo 1000 tick al secondo, la lettura iniziale può cadere tra due incrementi, e il task può essere eseguito soltanto dopo un ritardo di scheduling. Il nostro modello conta incrementi e non ricostruisce quella fase iniziale. Per una deadline fisica bisogna definire quando inizia il budget, quale sorgente temporale lo misura e quando l’azione di timeout diventa effettiva.
In una pipeline sensore-preprocessing-inferenza-attuatore, misurare soltanto l’attesa della rete neurale esclude altri contributi. Una politica che controlla la scadenza solo a fine inferenza può rilevare il ritardo senza impedirlo. L’aritmetica corretta del timer risponde a una domanda necessaria ma più stretta: quanti incrementi sono passati nelle condizioni del modello? Non dimostra una latenza massima, un percentile, un consumo o il rispetto del tempo reale dell’intera pipeline.
Per passare dal modello a una misura servirebbero una piattaforma identificata, la configurazione del tick, versioni di kernel e compilatore, protocollo di acquisizione e condizioni operative. Non riportiamo questi dati come se fossero stati misurati: non abbiamo una prova hardware in questo articolo. Anche l’interesse EL-AI per applicazioni embedded è una direzione editoriale e applicativa da esplorare, non evidenza che l’azienda abbia già una scheda o un’installazione con queste prestazioni.
La risposta: il numero zero non azzera il tempo trascorso
Il timeout va interpretato come intervallo. Nel caso svolto, partire da 65530 e arrivare a 14 significa che sono passati 20 tick, se sappiamo che l’intervallo reale è inferiore a 65536 tick. La differenza modulare conserva questa informazione anche attraversando lo zero. Se può essere passato un giro intero non osservato, due letture non bastano: occorre stato aggiuntivo o un vincolo temporale garantito. Riconoscere questo limite evita di scambiare una formula utile con una promessa universale di affidabilità.
Fonti, versioni e codice
M=65536
start=65530
duration=20
for elapsed in [0,5,11,19,20,26,65536]:
now=(start+elapsed)%M
delta=(now-start)%M
print(elapsed,now,delta,delta>=duration)
for start8 in range(256):
for elapsed8 in range(256):
now8=(start8+elapsed8)%256
assert (now8-start8)%256==elapsed8
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 21 ottobre 2026.