Chapter 4 Il modello di distribuzione

Uno dei requisiti di HELM (vedi 1.3.1) è quello di permettere a chiunque abbia uno spazio HTTP o FTP di pubblicare un proprio documento matematico, senza aver bisogno di far girare alcun programma sul lato server. Come conseguenza, per scaricare un documento è necessario conoscerne l'URL. L'utilizzo di URL per identificare i documenti che compongono la libreria di HELM non è, però, una buona scelta per diverse ragioni:

Scarsa efficienza e fault-tolerance Un URL identifica il server su cui risiede l'unica copia del documento. Pertanto, tralasciando la possibile esistenza di proxy o cache, il server rappresenta un collo di bottiglia per le prestazioni e un single point of failure¹.
Mancata rilocabilità dei documenti Modificare la posizione fisica di un documento, per esempio spostandolo su un altro server, cambia il suo URL, con conseguenti problemi di collegamenti interrotti (broken link). Questi sono inaccettabili, in particolar modo in una libreria di documenti matematici formali, in quanto di un oggetto si può fare il type-checking esclusivamente se sono accessibili tutti i documenti dai quali esso dipende.
Impossibilità per l'editore di un documento di cancellarlo È un problema strettamente legato al precedente, ma distinto. Può accadere che qualcuno pubblichi un documento che, a distanza di tempo, non ritenga più utile. Pertanto, deve essere libero di cancellarlo (qualsiasi affermazione contraria sarebbe, a dir poco, utopistica). Questa operazione, però, invalida tutti i documenti che da quello dipendono.

Un primo passo verso la soluzione dei precedenti problemi è l'identificazione dei documenti tramite nomi logici, che possono assumere la forma di URI, la cui sintassi viene descritta nell'RFC 2396. In particolare, il formato degli URI per gli oggetti CIC della libreria di HELM può essere molto semplice. Attualmente, come già spiegato nel paragrafo 3, associamo ad ogni documento un URI ottenuto anteponendo ``cic:/'' al suo path relativo al directory di base della libreria, eliminando poi il suffisso costante ``.xml''.

L'utilizzo di nomi logici fa nascere l'esigenza di una politica di naming per impedire che a documenti diversi venga assegnato lo stesso nome. Il problema, che non si pone nel caso degli URL, non è ancora stato affrontato e lo sarà solamente quando il progetto uscirà dalla fase sperimentale. Comunque, la soluzione più semplice è la creazione di una naming authority, che potrà essere centralizzata o distribuita. Altre soluzioni verranno comunque prese in considerazione.

Una volta introdotto l'uso di nomi logici, diventa possibile permettere l'esistenza di più istanze identiche di uno stesso documento, identificate dallo stesso URI. Opportuni strumenti, descritti nel prossimo paragrafo, si occuperanno della risoluzione dei nomi logici negli opportuni nomi fisici.

Se le occorrenze multiple dei documenti aprono la strada alla risoluzione dei problemi di bilanciamento del carico, fault-tolerance e rilocabilità dei documenti, generalmente introducono problemi di consistenza fra le differenti copie. Questi problemi sono assenti nell'ambito di HELM per via di una caratteristica peculiare dei documenti che descrivono oggetti matematici, che è la loro immutabilità: la correttezza di un oggetto A che dipende da un documento B può essere garantita solamente se B non cambia. L'immutabilità dei documenti garantisce automaticamente la consistenza fra le diverse copie. Inoltre, essa non impedisce l'esistenza di diverse versioni del documento, ma semplicemente la mutabilità di ognuna di queste. Per esempio, è ragionevole pensare di poter rilasciare una nuova versione del documento quando viene trovata la dimostrazione di una congettura.

Il terzo problema citato all'inizio del capitolo, legato all'impossibilità di cancellare i documenti, scompare in presenza di occorrenze multiple identificate dallo stesso nome logico. Infatti, anche per motivi prestazionali, diventa usuale effettuare copie locali dei documenti acceduti frequentemente o di quelli da cui dipendono le proprie teorie; inoltre, una volta effettuata la copia, questa può essere messa a disposizione di tutti. In questo modo, entra in azione un meccanismo di selezione naturale, per il quale i documenti più interessanti si diffondono rapidamente, mentre gli altri scompaiono quando ne viene cancellata anche l'ultima copia.

Forti sono le analogie fra i documenti della libreria di HELM ed i package utilizzati per l'installazione di programmi, per esempio nelle diverse distribuzioni del sistema operativo Linux. Infatti, affinché un programma possa venire mandato in esecuzione, le librerie installate nel sistema devono fornire le funzionalità attese, ovvero o devono non essere cambiate rispetto alla versione sulla quale è stato compilato il programma, oppure devono essere di una versione più recente e compatibile all'indietro. In sostanza, anche i package devono essere immutabili, ma deve essere possibile rilasciare una nuova versione del package quando il programma viene aggiornato. Inoltre, anche i package sono usualmente replicati su diverse macchine e vengono talvolta identificati da nomi logici. Pertanto, è naturale scegliere un modello di distribuzione simile.

In particolare, abbiamo adottato il modello utilizzato dalla distribuzione Debian², che si basa sul sistema Advanced Package Tool (APT), uno strumento che, in HELM, viene chiamato getter. Al getter APT viene fornita dall'utente una lista di server (HTTP, FTP, NFS, etc.) ordinata secondo un qualche criterio che, usualmente, è il tempo di accesso dovuto al carico del server e alla sua lontananza fisica. Su richiesta, APT contatta tutti i server della lista, che forniscono l'elenco dei package a loro disposizione (con le relative versioni). Con queste informazioni, APT costruisce un cache in cui associa ad ogni nome logico l'URL dell'istanza del pacchetto sul primo server della lista che lo fornisce. Successivamente, quando l'utente richiede il pacchetto, APT accede al proprio cache, individua l'URL, contatta il server corrispondente e scarica sul file-system la copia fornita.

Basandosi sul modello di APT, nel prossimo paragrafo descriveremo i requisiti e due diverse implementazioni di un getter per HELM.

4.1 Il getter

Queste sono le funzionalità di base che devono fornire i getter per HELM:

Un modo per l'utente di specificare un insieme di server da contattare e un insieme di regole da utilizzare per generare un ordinamento parziale, dipendente dal singolo documento, fra i server che lo forniscono.
Una funzione di update, da eseguirsi in modo batch, per costruire un cache che associ ad ogni URI un URL, basandosi sui due insiemi dati in precedenza.
Una funzione, chiamata get, che, dato un URI, restituisca il documento associato.

Altre funzionalità che i getter possono fornire sono:

Metodi intelligenti di scaricamento basati sulla località dei riferimenti. Per esempio, il getter potrebbe autonomamente effettuare il download di tutti i documenti riferiti dal documento scaricato e successivamente richiesti con alta probabilità.
Scaricamento di file compressi. Se il server che fornisce il documento lo fornisce, staticamente o su richiesta, anche o solamente in modalità compressa, il getter diventa responsabile non solo dello scaricamento, ma anche della successiva decompressione.
Scaricamento di più file contemporaneamente. Al getter potrebbe venire richiesto di effettuare il download di un insieme di file. La funzionalità diventa particolarmente interessante se combinata con le precedenti.
Ricostruzione ``al volo'' di documenti. Il getter potrebbe saper gestire URI che identificano documenti che debbono essere creati assemblando opportunamente informazioni ricavate da fonti distinte, per esempio effettuando la fusione di documenti residenti su diversi server o ottenuti contattando database remoti.

L'interazione fra il getter e i suoi client, infine, deve poter avvenire secondo le modalità a loro disposizione. Questo determina l'esigenza di avere più di una implementazione. Attualmente, infatti, sono stati sviluppati due diversi prototipi: il primo è un modulo OCaml che, una volta effettuato il download dei documenti, li salva su disco; il secondo si comporta come un server HTTP che restituisce i documenti scaricati come risultato delle richieste HTTP.

4.1.1 Il getter con interfaccia OCaml

Il primo prototipo sviluppato è un modulo OCaml, che è stato successivamente utilizzato nello sviluppo del proof-checker (vedi capitolo 5). Le sole funzionalità implementate sono state quelle di base. In particolare, serve un getter in grado di utilizzare un cache permanente su disco. In altre parole, ogni volta che il getter scarica un file, lo memorizza su disco e utilizza questa copia per le successive richieste.

Progettazione

La progettazione è stata estremamente semplice in quanto le richieste erano ben dettagliate. In particolare si è deciso che:

Ogni server, di tipo HTTP o FTP, mantiene i file della libreria di HELM strutturati secondo la gerarchia descritta nel precedente capitolo. Come conseguenza, alla radice della gerarchia resta associato un URL. Inoltre, un server può mantenere più gerarchie distinte identificandole con URL distinti.
Ogni server fornisce, nel directory base della gerarchia, un file contenente la lista degli URI di tutti gli oggetti esportati. Il formato del file può essere ragionevolmente sia testuale (un URI per linea), sia XML. Poiché la lista non deve subire elaborazioni particolari, a causa della banalità del parsing del formato testuale e per motivi di efficienza (le liste conterranno mediamente diverse migliaia di elementi), si è scelto di utilizzare il formato testuale, che richiede meno spazio su disco e tempi di parsing molto minori.
Ogni client mantiene un file di configurazione per ogni utente, con possibilità di condivisione del file, in cui viene elencata una lista ordinata di URL di gerarchie. Gli URL sono ordinati secondo l'ordine di preferenza crescente dell'utente per i vari server. Questa scelta corrisponde alla politica più semplice che soddisfa il primo requisito obbligatorio: l'ordinamento fra i server è totale e indipendente dall'URI particolare. Anche in questo caso il formato del file può essere ragionevolmente sia testuale che XML. Il numero degli elementi della lista, però, sarà sempre ragionevolmente basso e saranno sicuramente implementati in futuro vari tipi di elaborazioni sul file, quali modifiche, confronti, fusioni e riordinamenti. Pertanto, la scelta cade ragionevolmente sul formato XML, anche se, per il momento, l'implementazione utilizza un semplice file testuale³.
Ogni client mantiene, per ogni file di configurazione, un semplice database con una sola tabella in cui ad ogni URI viene associato l'URL ottimale, scelto in accordo con l'ordinamento del file. L'unica query possibile sul database è la richiesta di quale URL è associato ad un determinato URI. La struttura del database e la forma della query suggeriscono fortemente l'adozione come database di un file Berkeley DB, che a sua volta è usualmente implementato come un BTree e che è uno standard consolidato in ambiente Unix, ma di cui esistono implementazioni anche sotto altri sistemi operativi (es. Microsoft).
Vengono forniti tre moduli OCaml, il cui grafo delle dipendenze è mostrato in figura 4.1

Figura 4.1: Grafo delle dipendenze per i moduli dell'implementazione del getter come modulo OCaml

Il primo modulo, chiamato UriManager, fornisce il tipo di dato astratto uri, la funzione eq per determinare l'uguaglianza fra uri e due funzioni di conversione fra il tipo di dato astratto e la sintassi concreta, chiamate string_of_uri e uri_of_string. La signature del modulo è la seguente:
```
type uri
val eq : uri -> uri -> bool
val uri_of_string : string -> uri
val string_of_uri : uri -> string
 
```
Il secondo modulo, chiamato Configuration, ha la seguente signature:
```
val tmpdir : string
val indexname : string
val servers_file : string
val uris_dbm : string
val dest : string
 
```
dove servers_file è il path assoluto del file descritto al punto 3, uris_dbm quello del file Berkeley DB descritto al punto 4, indexname il nome del file descritto al punto 2, dest il path del cache e tmpdir il path del directory da utilizzare per la creazione di file temporanei. Il modulo deve essere implementato in modo da leggere i parametri da un file XML specificato in qualche modo dall'utente.

Il terzo modulo, chiamato Getter e dipendente dai precedenti, fornisce esclusivamente l'implementazione dei due metodi update e get, basata sulle decisioni prese nei precedenti punti. La signature del modulo è la seguente:
```
(* get : uri -> filename *)
val get : UriManager.uri -> string

(* synchronize with the servers *)
val update : unit -> unit
 
```
Il metodo update si occupa di rigenerare il database contattando tutti i server elencati nel file di configurazione. Il metodo get cerca in cache il file il cui URI viene dato come parametro. Se non lo trova, lo scarica utilizzando l'URL a cui l'URI è associato nel database e ne mette una copia in cache. In entrambi i casi ritorna il path assoluto del file in cache.

Si noti che, se il client è anche un server e il cache del client coincide con la gerarchia esportata, diventa possibile mettere a disposizione tutti i documenti acceduti semplicemente aggiungendo all'indice dei file esportati ogni file scaricato dal getter.

Implementazione

Accenniamo ai punti salienti dell'implementazione di due dei tre moduli OCaml, in quanto il restante, l'UriManager, non è interessante ai fini del modello di distribuzione e può essere implementato in modo banale istanziando il tipo di dato astratto con il tipo string, la funzione di confronto con l'uguaglianza polimorfa del linguaggio e le due funzioni di conversione con l'identità sulle stringhe⁴.

Per quanto riguarda il file di configurazione, si è scelto di utilizzare un file XML, di cui è stato fornito il DTD, avente per ogni parametro un elemento il cui nome sia lo stesso del parametro. Inoltre, per evitare di replicare più volte le stesse sotto-stringhe, è possibile utilizzare un elemento XML, il cui tag è ``value-of'', per effettuare interpolazione della variabile già definita il cui nome è indicato nell'attributo ``var''. Il modulo Configuration è stato quindi implementato ricorrendo a Markup⁵, un parser XML validante con ottime prestazioni⁶ implementato interamente in OCaml.

Il modulo Getter è stato implementato nella maniera più scontata, ricorrendo alla libreria standard di OCaml per la gestione dei file Berkeley DB e richiamando il programma wget⁷ per effettuare il download di un file dato l'URL. Vediamo più dettagliatamente le operazioni compiute dalle due funzioni:

update: Vengono scaricati, utilizzando wget, gli indici dei file esportati di tutti i server specificati dall'utente e letti dall'apposito file. A questo punto si svuota il database e, partendo dall'ultimo indice scaricato e procedendo a ritroso, si inseriscono nel database tutte le coppie URI---URL per le quali non è già stata inserita una coppia con lo stesso URI.
get: A partire dall'URI dato in input, si ricava il pathname del file in cache che sarà il valore ritornato. Se il file è già lí presente, la funzione termina; altrimenti, si ricava dal database l'URL da contattare e si usa wget per scaricare il file.

Il codice, anche grazie all'utilizzo di wget e Markup, risulta molto compatto: il modulo Getter richiede solo 111 righe di codice OCaml, commenti inclusi (99 senza commenti); Configuration 90 righe (76 senza commenti); l'implementazione banale di UriManager solo 3 righe prive di commenti. L'intera implementazione ha richiesto meno di un pomeriggio (5 ore uomo).

4.1.2 Il getter con interfaccia HTTP

Il secondo prototipo sviluppato viene richiamato dagli stylesheet descritti nel capitolo 6 quando è necessario accedere ad altri documenti, per esempio per conoscere i nomi dei costruttori dato l'URI, l'indice della definizione (co)induttiva del loro tipo e l'indice del costruttore. Poiché non esiste una maniera standard per estendere i processori XSLT con moduli per la risoluzione degli URI, si è scelto di fornire una seconda implementazione del getter sotto forma di (mini) server HTTP. Una soluzione alternativa era l'utilizzo di un CGI; questa, però, obbligava l'utente all'installazione di un server Web, di norma di cospicue dimensioni, che fornisse il supporto per i CGI. La nostra implementazione, al contrario, è caratterizzata dalla modestissima occupazione in memoria e su disco (uno script Perl di sole 183 righe, commenti inclusi).

Il mancato riutilizzo del modulo OCaml è ben motivato: poiché in OCaml non esiste alcuna libreria che implementi le funzionalità di un server HTTP, la complessità della realizzazione della libreria sarebbe stata ampiamente maggiore di quella della reimplementazione in un altro linguaggio. Inoltre, per motivi di efficienza, non è stato nemmeno possibile invocare il primo prototipo come programma esterno: questo, dopo aver scaricato un file, lo memorizza su disco con conseguente necessità di ricaricarlo in memoria per restituirlo al client HTTP⁸.

Progettazione

Anche in questo caso la progettazione, che si è pesantemente basata su quella del primo prototipo, è stata estremamente semplice. Si è deciso che:

Il file di configurazione, quello in cui vengono elencati i siti da contattare, il database e il cache su disco sono condivisi con il primo prototipo.
Il prototipo si comporta come un server HTTP, mettendosi in ascolto su una porta specificata dall'utente e rispondendo alle richieste i cui percorsi (ovvero la parte dell'URL che segue quella che identifica l'host) sono istanze dei seguenti schemi:
- /get?url=uri Utilizzato per chiedere una copia del documento il cui URI è uri.
- /annotation?url=uri Descritto nel capitolo 6
- /getdtd?url=nome Utilizzato per ottenere una copia del DTD il cui nome è nome⁹.
- /conf Utilizzato per sintetizzare un documento XML contenente alcuni dei parametri di configurazione del getter.
Per esempio, per richiedere la definizione del tipo induttivo dei numeri naturali al getter che gira sulla porta 8081 dell'host phd.cs.unibo.it, si utilizza il seguente URL:
``http://phd.cs.unibo.it:8081/get?uri=cic:/coq/INIT/Datatypes/nat.ind''
Il getter è implementato ricorrendo a due moduli Perl, dei quali uno è responsabile esclusivamente della gestione dei parametri di configurazione.

Implementazione

L'implementazione è stata estremamente banale grazie all'utilizzo delle seguenti librerie Perl:

HTTP::Daemon che implementa un semplice server HTTP che è facilmente personalizzabile scrivendo il codice che viene richiamato ogni volta che viene effettuata una chiamata al server. La libreria, inoltre, facilita la manipolazione di tutti i parametri, sia in entrata che in uscita, della richiesta HTTP.
LWP:UserAgent che implementa un client HTTP, gestendo tutti i dettagli della connessione.
DB_File che è una libreria per la gestione di vari tipi di database implementati come file, fra cui quelli Berkeley DB.
XML::Parser che implementa un semplice parser XML fornendo un'interfaccia ad eventi simile a SAX¹⁰.

Scendendo maggiormente in dettaglio, sono stati implementati due script Perl, configuration.pl e http_getter.pl. Il primo copre lo stesso ruolo del modulo OCaml Configuration, esportando omonime variabili. Il secondo, che utilizza il primo, implementa il server HTTP: ogni volta che viene ricevuta una richiesta, controlla se questa rientra in uno degli schemi di URL riconosciuti e¹¹

se la richiesta è di tipo conf, restituisce un documento XML creato al volo in cui vengono indicati alcuni dei propri parametri di configurazione.
se la richiesta è di tipo getdtd, carica il DTD richiesto da disco e lo restituisce.
se la richiesta è di tipo get, effettua le stesse operazioni eseguite dal metodo get del modulo Getter del primo prototipo; invece di restituire il nome del file, però, restituisce il contenuto del file scaricato o, se questo era già presente in cache, il contenuto della copia in cache.

Il codice, grazie all'utilizzo delle potenti librerie elencate precedentemente, è molto compatto: il modulo configuration.pl è di sole 35 linee, commenti inclusi; http_getter.pl è di 183 linee commenti inclusi (175 senza commenti). L'intera implementazione ha richiesto due giorni (20 ore uomo), incluso il tempo dedicato allo studio di alcune delle librerie.

1: L'affermazione deve essere mitigata. Nel caso in cui il server sia a sua volta un sistema distribuito con bilanciamento del carico e replicazione in spazio, i problemi citati non si presentano. Attualmente, però, la maggior parte degli utenti ha accesso esclusivamente a sistemi non fault-tolerant costituiti da un singolo host, per cui vale l'affermazione.
2: http://www.debian.org
3: Il passaggio al formato XML dovrebbe avvenire a breve.
4: Per una implementazione nient'affatto banale data durante lo sviluppo del proof-checker, si veda il paragrafo 5.1.1.
5: http://www.ocaml-programming.de/packages/documentation/pxp
6: Nel solo parsing di tutti i file XML che compongono la libreria standard di Coq, Markup è risultato circa 5 volte più veloce del parser validante per SGML scritto in C da J. Clark e chiamato SP (SGML Parser) e ha avuto approssimativamente le stesse prestazioni di expat che è un parser XML non validante scritto in C sempre da J. Clark.
7: wget è un utility free, sviluppato dal consorzio GNU, per il download non interattivo di singole pagine o di interi siti. Può utilizzare indistintamente i protocolli HTTP o FTP.
8: Il server potrebbe efficientemente restituire al client la locazione su disco del documento, in conformità al protocollo HTTP. Questa opzione non è , però, possibile, in quanto il prototipo, come descritto nel capitolo 6, effettua anche sintesi al volo di file ottenuti a partire da più di un documento alla volta.
9: I DTD in HELM non vengono identificati da un URI, ma semplicemente dal loro nome.
10: SAX è un'interfaccia ad eventi per i parser XML che è diventata uno standard di fatto in ambiente Java.
11: Le operazioni compiute se la richiesta è di tipo annotation verranno descritte nel capitolo 6.