Ricostruzione di tipi per l'analisi di deadlock e lock nel pi-calcolo lineare

In recent years, the traditional sequential programming paradigm has been substituted by service-oriented computing, a new paradigm for the development of software systems based on the internalisation of the concept of distributed service. In this paradigm, the computational behaviour of a system is organised into a collection of services, which run concurrently and interact with each other, instead of being organized into a collection of functions running sequentially. The reason behind the broad diffusion of this software architecture is that, splitting the applications business logic and presentation layer in micro-services, it is easier to scale out compute resources (e.g. using cloud computing), better responding to the grown of costumers. Moreover, service-oriented applications are more fault tolerant than the sequential ones: services replication is simpler and crashes do not compromise the availability of the whole system. From the programmers point of view, the development of these systems could be really hard. The support of distributed communication in the major programming languages, such as Java, C#, Python, Javascript and C++, is available only as external libraries (APIs). This lack of language-level support means that communication patterns are not visible to compilers or to program analysis tools. For example, implementing a login service requires a complex interaction with external services calls. If this is represented only as a sequence of API calls, with no explicitly-defined high-level structure, then programming errors are easy to make and difficult to detect. These difficulties in the service-oriented infrastructures development, have stimulated the scientific community to create many type theories for distributed computing systems. Built on the formal foundations provided by process calculi, such as CSP, CCS and pi-calculus, these methods make use of rich types to describe communication and provide deduction rules to prove the well-behaviorness of software systems. The implementation of such systems in real-world programming languages would require programmers to modify their coding habits providing, together with the code, extra informations (annotations) regarding the use their programs make of communication channels. For that reason, the ``test it, fix it'' approach is still the most popular among developers. In order to overcome these limitations, in this thesis we study a type reconstruction algorithm for the deadlock and lock free linear pi-calculus, a refinement of the linear pi-calculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). Starting from code (without any extra information), our algorithm automatically infers all the informations needed to prove programs well-behaviorness without requiring any aid from programmers. Together with its formal definition, we discuss some aspect concerning hypha, the proof-of-concept implementation of the algorithm and some examples of real-world communication patterns, such as full-duplex, that we used as benchmark.

Negli ultimi anni, il tradizionale paradigma di programmazione sequenziale è stato sostituito dal "service-oriented computing", un nuovo approccio allo sviluppo di sistemi software basato sul concetto di servizio distribuito. Al posto che essere organizzati in una collezione di funzioni sequenziali, i sistemi sviluppati secondo il paradigma SOA fanno uso di una serie di servizi contemporaneamente in esecuzione che interagiscono l'uno con l'altro per portare a termine la computazione. Le principale giustificazione alla rapida diffusione di questa architettura software è che, separando la "business logic" delle applicazioni e il "presentation layer" in micro-servizi, è più facile scalare rispetto alle risorse di calcolo (usando, per esempio, infrastrutture di cloud computing), rispondendo con maggiore flessibilità alla crescita del carico applicativo. Inoltre, le applicazioni "service-oriented" sono per definizione più resistenti ai fallimenti di quelle sequenziali: la replica dei servizi, infatti, è molto più semplice ed un crash di un singolo micro-servizio non compromette la disponibilità dell'intero sistema. Dal punto di vista dei programmatori, lo sviluppo di questi sistemi può essere molto difficile. Il supporto alla comunicazione distribuita nei maggiori linguaggi di programmazione, come Java, C#, Python, Javascript, C++, è disponibile solo per mezzo di librerie esterne (API) e non è quindi possibile sfruttare l'ausilio del compilatore per identificare possibili errori nell'utilizzo dei protocolli di comunicazione. Queste difficoltà nello sviluppo di sistemi software "service-oriented" hanno stimolato la comunità scientifica alla creazione di diverse teorie di tipi specifiche per i sistemi distribuiti. Sfruttando come linguaggio algebre di processi come CSP, CCS e il pi-calcolo, questi metodi fanno uso di tipi molto ricchi per descrivere la comunicazione e forniscono delle regole di deduzione per dimostrare la correttezza dei sistemi software. L'adozione diretta di questi sistemi nei linguaggi di programmazione reali richiederebbe ai programmatori di modificare le loro abitudini di programmazione annotando il codice con informazioni riguardanti l'uso che i loro programmi fanno dei canali di comunicazione. Per questa ragione l'approccio "test it, fix it" è ancora il più diffuso da chi sviluppa questo genere di software. Con l'obbiettivo di superare questi ostacolo, in questa tesi studiamo un algoritmo di inferenza per il pi-calcolo lineare deadlock free e lock free, un raffinamento del pi-calcolo lineare che garantisce l'assenza di deadlock (la possibilità che un processo si blocchi con delle operazioni di input output non concluse) e l'assenza di lock (la possibilità che un processo non termini mai le operazioni di input output in sospeso). Partendo dal codice scritto dai programmatori (senza annotazioni aggiuntive), il nostro algoritmo inferisce in maniera automatica tutte le informazioni necessarie alla verifica del corretto comportamento dei programmi. Nel corso della trattazione presentiamo inoltre hypha, un'implementazione sperimentale dell'algoritmo realizzata in Haskell e ne discutiamo le performance con l'ausilio di una suite di test appositamente creata.