Estudio y desarrollo de técnicas para el testing de programas concurrentes

Estudio y desarrollo de t´ecnicas para el testing de programas concurrentes Universidad Complutense de Madrid Facultad de Inform´ atica Trabajo de fin de grado del Doble Grado en Matem´ aticas e Ingenier ´ ıa Inform´ atica Marco Antonio Garrido Rojo Dirigido por: Miguel G´omez-Zamalloa Gil Curso 2017-2018 Copyright c Marco Antonio Garrido Rojo Este trabajo puede encontrarse en https://github.com/MaSteve/CABS-Memoria bajo licencia MIT. Resumen El avance de los ordenadores en las ´ultimas d´ecadas ha brindado la oportunidad a los desarrolladores de programas de aprovechar las ventajas de los procesadores modernos que permiten la ejecuci´on simult´anea de varios hilos de ejecuci´on al mismo tiempo. Es por este motivo por el que cada vez es m´as com´un el desarrollo de programas concurrentes en todos los ´ambitos, desde el software cient´ıfico hasta las aplicaciones m´oviles. No obstante, el desarrollo de programas concurrentes conlleva riesgos adicionales como deadlocks o condiciones de carrera no presentes en los programas secuenciales. Es por ello necesario el uso de t´ecnicas de validaci´on como el testing para poder comprobar el comportamiento de los programas y verificar que cumplen con los requisitos adecuados. Sin embargo, las t´ecnicas de testing habituales no son efectivas debido al indeterminismo en la ejecuci´on de los procesos y una exploraci´on exhaustiva de todos los posibles entrelazamientos suele ser intratable por su coste exponencial. No obstante, en los sistemas basados en actores, debido a la ausencia de memoria compartida y la ejecuci´on sin interrupciones de los procesos, el n´umero de puntos en los que hace falta considerar el indeterminismo de estos programas es mucho menor. Una de las mejores t´ecnicas para mitigar la explosi´on de estados es el algoritmo POR (Partial Order Reduction), que permite agrupar en clases de equivalencia derivaciones redundantes, y sobre el que, hoy en d´ıa, se sigue investigando. Sobre estas l´ıneas en este trabajo nos centraremos en el uso de SYCO para el testing de programas concurrentes. SYCO es una herramienta para ABS, un lenguaje de modelado para programas concurrentes basado en el modelo de actores, que permite obtener los posibles estados finales de un programa concurrente usando el estado del arte del algoritmo DPOR (Dynamic Partial Order Reduction). No obstante, el problema que presenta ABS es que, como todo lenguaje de modelado, la implementaci´on real de un programa dista mucho de la implementaci´on que se pueda hacer en este lenguaje. Adem´as, el modelo de concurrencia basado en actores, pese a estar cobrando cada vez m´as importancia, no es el modelo de los lenguajes m´as populares como son Java y C/C++. La idea de este trabajo consiste en facilitar el uso de las herramientas de testing implementadas para ABS con los programas escritos en C. Para ello desarrollaremos un lenguaje con una sintaxis similar a C, llamado CABS, que permitir´a la ejecuci´on concurrente de hilos, usando para ello una concurrencia de grano fino. Abstract The advance in computers during the last decades has brought the opportunity to take advantage of the new processors which are able to execute several threads at the same time. That is the reason why concurrent programs are getting more and more common in a wide variety of situations, including, for example, scientific software and mobile apps. Nevertheless, concurrent software development has additional risks, such as deadlocks and data races, which are not present in sequential programs. That is why it is necessary to use validation techniques, such as software testing, in order to check the behavior of these programs and their requirements. However, the usual techniques are not effective due to the nondeterministic behavior of these programs and trying to search all the possible interleavings is an intractable problem due to its exponential cost. However, in the actor model paradigm, due to the absence of share memory and the non-preemptive scheduling, the number of interleavings is much lower. One of the best techniques for avoiding the state explosion is the Partial Order Reduction (POR) algorithm. This algorithm can merge several redundant derivation into the same equivalence class. Nowadays, some researchers are still working on this. In this thesis, we will use a specific implementation of this technique, called SYCO. SYCO is a software tool developed for ABS, a modeling language for concurrent programming based on the actor model. Using this tool, we can obtain the possible final states of a concurrent program using the state of the art in the Dynamic Partial Order Reduction (DPOR) algorithm. However, ABS implementations are far away from a real implementation of the final program in one of the main languages, such as Java or C/C++. In addition, actor model concurrency is not the paradigm used in those languages. The idea of this thesis is to develop a programming language, similar to C, with a finegrain concurrency support and to make easier the use of the tools developed for ABS in C programs. The name of this language is CABS. (Did you catch the joke?) Palabras clave ABS SYCO Programas concurrentes Sem´anticas Lenguaje de programaci´on Interleavings Testing de programas Modelo de concurrencia basado en actores CUP JLEX Keywords ABS SYCO Concurrent programming Semantics Programming languages Interleavings Software testing Actor model concurrency CUP JLEX 16 CAP´ ITULO 1. INTRODUCCI ´ ON algo m´as interesante. Este concepto es conocido como paso de mensajes. Cada hilo de ejecuci´on ahora podr´a en un momento dado escuchar el canal o escribir en ´el y modificar su comportamiento seg´un los mensajes que reciba. Seguimos por tanto contando con los mismos problemas de la concurrencia reduciendo eso s´ı el n´umero de interleavings a tener en cuenta. Imaginemos ahora que los mensajes mandados entre objetos son los que provocan la ejecuci´on de los m´etodos que estos contienen. Esta es la idea en los modelos de concurrencia basados en actores. En estos modelos, cada objeto ejecuta sus tareas de forma concurrente con respecto a las del resto de objetos con la ´unica restricci´on de que cada objeto solo puede ejecutar una ´unica tarea a la vez. El resto de tareas esperan en una cola cuyo orden en principio no es determinable. El paso de mensajes indica qu´e m´etodo desea ejecutar un objeto (pudiendo ser uno propio o perteneciente a otro objeto) y, dependiendo del tipo de llamada, una tarea puede dejar paso a otra si a´un no cuenta con los valores necesarios para proseguir. Se trata de una concurrencia donde el scheduler o planificador no puede desasignar a una tarea dentro de un objeto si esta no ha terminado o si no ha llegado a un punto de espera, funcionando cada objeto como una especie de monitor. Esto es lo que se conoce como un modelo non-preemptive. Al igual que como hemos comentado anteriormente, al introducir los modelos de paso de mensajes, el modelo de actores tambi´en reduce notablemente el n´umero de interleavings a tener en cuenta. Esto es de vital importancia cuando se intentan aplicar t´ecnicas de testing sistem´atico en las que se deben de tener en cuenta todos los entrelazamientos posibles y donde hay que tener muy en cuenta la explosi´on de estados, que hace que sean intratables en los casos generales. Para estos m´etodos de exploraci´on sistem´atica se puede suponer que todas las instrucciones de una tarea se ejecutan una detr´as de otra sin ning´un entrelazamiento hasta que no se llega al final de la funci´on en un return. En este tipo de concurrencia se basan muchos lenguajes de programaci´on como por ejemplo Erlang y Scala, adem´as de ABS, el que va a ser nuestro compa˜nero de viaje en este trabajo. La motivaci´on de este trabajo es la creaci´on de un lenguaje de programaci´on b´asico, llamado CABS, que permita recrear una concurrencia entre procesos a nivel de grano fino y sobre el que podamos emplear las potentes herramientas ya elaboradas para el lenguaje ABS en la materia del an´alisis de programas concurrentes. CABS ser´a un lenguaje de programaci´on con una sintaxis parecida a la de C con tipado estricto y est´atico, que incluye la posibilidad de usar funciones y arrays y que se mueve en el paradigma de la programaci´on imperativa. Sobre esta tem´atica se han hecho ya trabajos similares de creaci´on de lenguajes o compiladores como en [1]. En dicho trabajo, se abord´o la detecci´on de deadlocks en un lenguaje b´asico que contaba con primitivas para declarar procesos y cerrojos y que empleaba la 17 herramienta SACO desarrollada para ABS sobre una traducci´on formal. De un modo similar, en nuestro trabajo emplearemos las mismas t´ecnicas formales sobre sem´anticas para demostrar que la traducci´on que se propondr´a para CABS en efecto cumple con la preservaci´on de todos los interleavings posibles y que, por tanto, los estados finales alcanzables ejecutando CABS con su sem´antica son los mismos que obtendr´ıamos con ABS. A diferencia de [1], nuestro trabajo pretende llegar a desarrollar un lenguaje de programaci´on Turing completo sobre el que se puedan implementar algoritmos y no restringirnos a crear una demostraci´on meramente acad´emica sobre la posibilidad de obtener los entrelazamientos en un lenguaje de prueba. De un modo similar al que se pretende hacer con CABS, en los a˜nos 80 se creo SPIN 1. SPIN es una herramienta de verificaci´on de sistemas distribuidos desarrollada por Gerard J. Holzmann que trabajaba sobre modelos escritos en Promela 2, un lenguaje de modelado, que era traducido a C. Era sobre el c´odigo en C donde se empleaban distintas t´ecnicas de verificaci´on, entre las que se inclu´ıa el uso de Partial Order Reduction (POR). En este aspecto, nosotros podremos aprovechar la herramienta SYCO, disponible para ABS y que implementa t´ecnicas avanzadas de Dynamic Partial Order Reduction (DPOR). Sobre esta herramienta dedicaremos un cap´ıtulo completo al final de este trabajo. El objetivo de DPOR es conseguir reducir el n´umero de estados de exploraci´on necesarios para conocer los posibles resultados finales de un programa. Como hemos visto en los ejemplos anteriores, existen ocasiones en que el orden en la ejecuci´on de dos instrucciones pertenecientes a procesos distintos no influye en el resultado final del programa y es en este aspecto donde DPOR consigue determinar que ordenes son redundantes para intentar salvar la explosi´on exponencial de estados intermedios. En un ´ambito m´as general podemos encontrar investigaciones como en [2], donde el uso de estas t´ecnicas se emplea para el an´alisis de Redes definidas por software o SDN por sus siglas en ingl´es. SDN es un paradigma sobre la arquitectura de redes que permite un control sobre el comportamiento de las mismas. En [2] se establece una relaci´on formal entre las SDN y el modelo de actores para la verificaci´on de software distribuido, realizando una especificaci´on en ABS. Como hemos podido ver, el terreno de la verificaci´on formal de programas concurrentes presenta ejemplos similares a los que intentaremos acometer en este trabajo que dividiremos en varios cap´ıtulos, cada uno de ellos centrado en un aspecto concreto. En los siguientes cap´ıtulos describiremos la sintaxis y sem´antica de nuestro lenguaje as´ı como la del lenguaje ABS sobre el que realizaremos la traducci´on de CABS. Posteriormente se demostrar´a la idea de la correcci´on de la traducci´on, lo que nos permitir´a extrapolar las propiedades del c´odigo ABS traducido al c´odigo original en CABS. Entre estas propiedades pueden encontrarse las resultantes del uso de herramientas formales desarrolladas sobre ABS. Tras toda la formalizaci´on, hablaremos de la implementaci´on de la traducci´on propuesta en un compilador de CABS a ABS, que desarrollaremos en Java usando JLex y CUP, herramientas empleadas en la asignatura de Procesadores de Lenguaje. Por ´ultimo, hablaremos de la aplicaci´on principal del compilador de CABS que es el uso de la 1https://en.wikipedia.org/wiki/SPIN_model_checker 2https://en.wikipedia.org/wiki/Promela 18 CAP´ ITULO 1. INTRODUCCI ´ ON herramienta SYCO para obtener todos los posibles resultados finales de la ejecuci´on de un programa concurrente aprovechando el state of the art en DPOR. ¡Comencemos! Cap´ıtulo 2 Sintaxis y sem´antica 2.1. Sintaxis de CABS La mayor´ıa de lenguajes de programaci´on del mercado siguen una sintaxis com´un similar a la que tiene el lenguaje original en el que se suelen basar que es C. A la hora de definir la sintaxis de CABS tomaremos como referencia de nuevo la de ese lenguaje. Para sentar las bases de la notaci´on que se usar´a de ahora en adelante para definir la sem´antica de nuestro lenguaje, diremos que Pes un programa en CABS formado por instrucciones globales como lo son las declaraciones de variables globales y las declaraciones de funciones. La declaraci´on de variables constar´a de un tipo y de un nombre de variable seguido de un punto y coma. Las funciones estar´an formadas por un tipo de retorno, un nombre de funci´on, una lista de argumentos (es posible que sea vac´ıa), un cuerpo con instrucciones S∈Stm y una expresi´on de retorno. A modo de ilustraci´on podemos ver el siguiente c´odigo 1type global_var1 ; 2type global_var2 ; 3 4type nombre_de_funcion (args ...) { 5... 6codigo 7... 8return exp 9} donde se muestra la declaraci´on de dos variables globales y de una funci´on. Los tipos que manejaremos en nuestro lenguaje ser´an enteros y booleanos, cuyos identificadores ser´an int ybool respectivamente. Permitiremos adem´as la declaraci´on y el uso de arrays de enteros y booleanos en asignaciones y expresiones aritm´etico-l´ogicas y como argumentos de funciones. No se podr´an usar como tipo de retorno. Un ejemplo del uso de arrays es el siguiente: 19 20 CAP´ ITULO 2. SINTAXIS Y SEM ´ ANTICA 1int array [10]; # Array global con 10 enteros 2int global_var ; # Aventuramos que valdra 27, pero eso dependera de la semantica :) 3 4int f(int res , int arr [10]) { 5int var; 6var = 2 * res + arr [1]; 7return var; 8} 9 10 int main () { 11 array [0] = 10; 12 array [1] = 5; 13 int res; 14 res = array [0] + 1; 15 global_var = f(res , array); 16 return 0; 17 } Las instrucciones Sdel cuerpo de una funci´on de un programa son las t´ıpicas de un lenguaje imperativo, entre las que se encuentran las asignaciones, las operaciones aritm´eticol´ogicas, las instrucciones de control, como los condicionales y los bucles y, la clave de un lenguaje con concurrencia, un thread para la ejecuci´on de funciones en paralelo imitando el comportamiento de la librer´ıa pthread en C. Veamos un ejemplo que use esta ´ultima construcci´on: 1int var; 2 3int main () { 4thread f(1); 5thread f(2); 6return 0; 7} 8 9void f(int value ) { 10 var = value ; 11 } Como podemos ver, las llamadas concurrentes son similares a las llamadas a procedimientos habituales precedidas por la palabra reservada thread. 2.2. Sem´antica de CABS A continuaci´on pasamos a hablar de la sem´antica del lenguaje CABS. La idea es dar un significado al c´odigo CABS de modo que quede definido el comportamiento de cada una de las construcciones presentes en el lenguaje. Para este prop´osito escogeremos una sem´antica de paso corto en la que la derivaci´on se puede interpretar como una secuencia 2.2. SEM ´ ANTICA DE CABS 21 de pasos que simulan las transiciones que generar´ıa un c´odigo ejecutado en un ordenador real, es decir, los cambios en memoria y en la instrucci´on actual marcada por un contador de programa. En una primera secci´on daremos las definiciones b´asicas de lo que ser´an los estados de nuestro programa para, posteriormente, especificar cuales ser´an las reglas que marcar´an las transiciones entre ellos. Por ´ultimo, mostraremos algunos ejemplos de derivaci´on a partir de unos programas b´asicos. 2.2.1. Pre´ambulo sem´antico Los programas en CABS se pueden entender, de forma simplificada, como unas secuencias de pasos que van a manejar unos valores enteros y l´ogicos posiblemente almacenados en una memoria donde tambi´en se guardar´an los resultados desprendidos de las operaciones que se realicen. Es por esto que en primer lugar tenemos que definir un conjunto de valores V=Z∪Bque sea la uni´on de los enteros y de los booleanos, los elementos b´asicos de todo programa. Una primera parte de la representaci´on del estado estar´a formada por las variables globales de nuestro programa. Definimos G=Var ,→Vel conjunto de funciones parciales del conjunto de variables al conjunto de valores. El estado actual de nuestras variables globales ser´a una funci´on de este conjunto y por lo general nos referiremos a ella con la letra G. Posteriormente cuando hablemos de variables locales tambi´en las definiremos como un conjunto de funciones similares pero que trataremos por separado por comodidad. El conjunto Var contiene todos los nombre de variable posibles y usaremos Gvar para referirnos al valor almacenado por la variable global var. Por ser una funci´on parcial quedan reflejadas en G´unicamente las variables que han sido previamente declaradas. Por otro lado nos encontramos en nuestro lenguaje con la necesidad de definir un conjunto que recoja la informaci´on b´asica de las funciones y procedimientos. Definimos F=Func ,→(T×Stm ×Args ×(Exp ∪ {ε})) el conjunto de funciones parciales que asocia un nombre de funci´on a su definici´on. Una funci´on quedar´a definida por su tipo de retorno t∈T, su c´odigo S∈Stm, sus argumentos de entrada arg ∈Args y su expresi´on de retorno e∈Exp ∪ {ε}. Seg´un las necesidades, la expresi´on de retorno ser´a una expresi´on booleana, una expresi´on aritm´etica o simplemente ser´a la expresi´on vac´ıa, empleada para los procedimientos. De nuevo tenemos un conjunto de nombres de funciones Func. En principio los nombres de variable y de funci´on son los mismos en los lenguajes de programaci´on habituales y es tambi´en el caso de CABS, no obstante, por simplicidad, consideraremos en la sem´antica que son conjuntos separados. A su vez, contamos tambi´en con la ventaja de las funciones parciales en Fque solo tendr´an la informaci´on de aquellas funciones que en verdad hayan sido definidas en el programa. Fser´a la metavariable que usaremos para referirnos a una funci´on de Fconcreta. Para dar un significado a nuestros programas tenemos que definir qu´e va a representar para nosotros su estado de ejecuci´on. Definimos el conjunto de estados State =G×F×RP como una tupla que recoja la informaci´on de las variables globales y de las funciones 22 CAP´ ITULO 2. SINTAXIS Y SEM ´ ANTICA definidas en nuestro programa P, as´ı como, una lista de marcos de ejecuci´on o runtime processes que contendr´a la informaci´on local de los procesos. Esto ´ultimo quedar´a recogido en los elementos de RP = ((Loc)+×Stm)∗donde Loc =Var ,→Vser´a el conjunto de ´ambitos locales. Por lo general usaremos la notaci´on local :s∈(Loc)+para referirnos a la pila de llamadas de un proceso, donde local ∈Loc ys∈(Loc)∗, emulando la notaci´on de lista de un lenguaje funcional como Haskell. Usaremos adem´as la metavariable RP para referirnos a una lista de marcos de ejecuci´on concreta y el operador ;para referirnos a un elemento de la lista cualquiera, de modo que, RP ;(local :s, S) indica que la lista de marcos RP contiene en concreto el marco (local :s, S) donde Ses el c´odigo del proceso y (local :s) su pila de ´ambitos locales. La idea a seguir para definir nuestra sem´antica ser´a apoyarnos en dos funciones auxiliares init ystart que respectivamente inicializar´an el estado global del programa y lanzar´an a ejecuci´on la funci´on inicial main, bas´andonos en la definici´on que hemos dado de estado. La funci´on init. Definimos la funci´on init :Prog ,→State de forma recursiva del siguiente modo. init(ε)=(nil,nil,[]) init(int var; P)=(G[ var 7→ 0] ,F,RP) donde init(P) = (G,F,RP) init(bool var; P)=(G[ var 7→ FALSE],F,RP) donde init(P) = (G,F,RP) init(int func(arg){S;return a}P)=(G,F[func 7→ (int, S, arg, a)] ,RP) donde init(P) = (G,F,RP) init(bool func(arg){S;return b}P)=(G,F[func 7→ (bool, S, arg, b)] ,RP) donde init(P) = (G,F,RP) init(void func(arg){S}P)=(G,F[func 7→ (void, S, arg, ε)] ,RP) donde init(P) = (G,F,RP) Con esta funci´on conseguimos crear el ´ambito global de variables y de funciones de nuestros programas en CABS. Hemos usado la notaci´on [x7→ value] para indicar que el valor de una funci´on en xes sustituido por el nuevo valor value. Esta notaci´on se seguir´a usando m´as adelante. La funci´on (regla) start. Definimos la funci´on start :State ,→State como start((G,F,RP)) = (G,F,[(nil : [], S)]) donde F(main)=(int, S, arg,0) Con esto conseguimos crear un nuevo marco de ejecuci´on con el c´odigo inicial de main. N´otese que la funci´on inicializa la pila de ´ambitos de variables locales con el ´ambito nil que no contiene ninguna variable inicializada. 2.2. SEM ´ ANTICA DE CABS 23 Sem´antica (Expresiones aritm´etico-l´ogicas). Las primeras reglas que queremos definir ser´an las de las expresiones aritm´etico-l´ogicas. Nuestro lenguaje permite la llamada a funciones con valor de retorno, lo que hace que tengamos que, desde un principio, manejar unas reglas que garanticen la no terminaci´on de la evaluaci´on de las expresiones. Ser´a por ello que tengamos que dar una definici´on de una funci´on parcial que dada una expresi´on nos devuelva otra expresi´on m´as simplificada, pudiendo emplear el estado del programa para ello y permitiendo modificaciones del mismo, hasta eventualmente quedarnos con un valor v∈V, lo que consideramos la expresi´on m´as simplificada. Empecemos por dar una definici´on en el caso de las expresiones enteras. De ahora en adelante nos referimos por el conjunto Aexp a la uni´on de expresiones aritm´eticas y valores enteros. Buscamos definir la funci´on sem´antica A: (Aexp×State),→(Aexp ×State) mediante las siguientes reglas: 24 CAP´ ITULO 2. SINTAXIS Y SEM ´ ANTICA [numA]hn, (G,F,RP ;(s, S))i →Aexp hN JnK,(G,F,RP ;(s, S))i local(x) = v varL Ahx, (G,F,RP ;(local :s, S))i →Aexp hv, (G,F,RP ;(local :s, S))i G(x) = v local(x) = undef varG Ahx, (G,F,RP ;(local :s, S))i →Aexp hv, (G,F,RP ;(local :s, S))i donde xes variable entera. ha1,(G,F,RP ;(s, S))i →Aexp ha0 1,(G,F,RP ;(s0, S0))i J1 Aha1Ja2,(G,F,RP ;(s, S))i →Aexp ha0 1Ja2,(G,F,RP ;(s0, S0))i ha2,(G,F,RP ;(s, S)))i →Aexp ha0 2,(G,F,RP ;(s0, S0)))i J2 AhvJa2,(G,F,RP ;(s, S)))i →Aexp hvJa0 2,(G,F,RP ;(s0, S0)))i J3 Ahv1Jv2,(G,F,RP ;(s, S))i →Aexp hv1JNv2,(G,F,RP ;(s, S))i donde Jes alguno de los operadores del lenguaje que tienen su hom´ologo sem´antico JN. ha, (G,F,RP ;(s, S))i →Aexp ha0,(G,F,RP ;(s0, S0))i unstack1 AhUNSTACK (a),(G,F,RP ;(s, S))i →Aexp hUNSTACK (a0),(G,F,RP ;(s0, S0))i unstack2 AhUNSTACK (v),(G,F,RP ;(local :s, S))i →Aexp hv, (G,F,RP ;(s, S))i F(func) = (int, SF, argsF, a)check args(argsF, args)eval(args) = args0 call1 Ahfunc(args),(G,F,RP ;(local :s, S))i →Aexp hfunc(args0),(G,F,RP ;(local :s, S))i 2.2. SEM ´ ANTICA DE CABS 25 F(func) = (int, SF, argsF, a)check args(argsF, args)eval(args) = v1:· · · :vn call2 Ahfunc(args),(G,F,RP ;(local :s, S))i →Aexp hUNSTACK (a),(G,F,RP ;(nil [args 7→ v1:· · · :vn] : local :s, SF;S))i donde check args es una funci´on auxiliar que comprueba la correcci´on de tipos y el n´umero de argumentos y donde eval indica que los argumentos de la funci´on son evaluados hasta conseguir los valores de Vfinales, haciendo uso de las reglas de la sem´antica de expresiones. De este modo se justifica que para ejecutar una funci´on sea necesario evaluar uno a uno los argumentos de la funci´on. De hecho, eval puede hacer uso de las reglas para expresiones booleanas en el caso de las funciones con par´ametros mixtos. Dichas reglas son las que definen B: (Bexp ×State),→(Bexp ×State). [TrueB]htrue, (G,F,RP ;(s, S))i →Bexp htrue,(G,F,RP ;(s, S))i [FalseB]hfalse, (G,F,RP ;(s, S))i →Bexp hfalse,(G,F,RP ;(s, S))i local(x) = v varL Bhx, (G,F,RP ;(local :s, S))i →Bexp hv, (G,F,RP ;(local :s, S))i G(x) = v local(x) = undef varG Bhx, (G,F,RP ;(local :s, S))i →Aexp hv, (G,F,RP ;(local :s, S))i donde xes una variable booleana. hb1,(G,F,RP ;(s, S))i →Bexp hb0 1,(G,F,RP ;(s0, S0))i J1 Bhb1Jb2,(G,F,RP ;(s, S))i →Bexp hb0 1Jb2,(G,F,RP ;(s0, S0))i hb2,(G,F,RP ;(s, S)))i →Bexp hb0 2,(G,F,RP ;(s0, S0)))i J2 BhvJb2,(G,F,RP ;(s, S)))i →Bexp hvJb0 2,(G,F,RP ;(s0, S0)))i J3 Bhv1Jv2,(G,F,RP ;(s, S))i →Bexp hv1JBv2,(G,F,RP ;(s, S))i 32 CAP´ ITULO 3. ABS: SINTAXIS Y SEM ´ ANTICA donde los argumentos son una lista separada por comas de cero o m´as nombres de variables precedidos de su tipo (al estilo de Java). De los tipos predefinidos en ABS solo usaremos los enteros (Int) y los booleanos (Bool). Tambi´en emplearemos el tipo gen´erico List para la construcci´on de Arrays. La declaraci´on de clases en ABS es similar a la de Java con la peculiaridad de que todas las clases definidas por el usuario deben implementar una interfaz. La sintaxis para la definici´on de clases en ABS es 1class nombre_de_clase ( args) implements nombre_de_interfaz { 2... 3declaraciones de atributos privados 4... 5... 6implementaciones 7... 8} La declaraci´on de atributos de una clase es id´entica a la de Java, con la ausencia de las palabras reservadas private,public oprotected. La visibilidad de todos los atributos es privada. Del mismo modo, las implementaciones de m´etodos siguen el mismo estilo. Un m´etodo es por tanto p´ublico si est´a definido en la interfaz que implementa la clase, en caso contrario es privado. Una caracter´ıstica especial de las clases de ABS es la posibilidad de definirlas con una lista de argumentos accesibles desde cualquier punto de la clase. Esta propiedad ser´a ampliamente explotada con posterioridad para la implementaci´on del concepto de variable global. Por ´ultimo, nos queda discutir las llamadas a m´etodos de una clase. En ABS, las llamadas a m´etodos son un paso de mensaje, es decir, cuando un objeto llama a un m´etodo de otro objeto o de s´ı mismo, dicha llamada se mete en una cola a la espera de poder ser ejecutada por el objeto receptor. Un objeto (o actor) solo puede ejecutar un mensaje a la vez. De los operadores de llamada a m´etodos de ABS, nosotros solo nos preocuparemos del operador ‘!’, cuya sintaxis es 1Fut <t_ret > ret = o!f(args ); La idea de esta llamada es mandar un mensaje al objeto opara que ejecute su m´etodo f. Esta llamada devuelve un tipo futuro. El tipo futuro permite entre otras cosas saber cuando se ha concluido la ejecuci´on del mensaje y en este caso recuperar el valor de retorno del m´etodo. Cuando queramos realizar una llamada s´ıncrona, es decir, una llamada para la que no deseamos continuar la ejecuci´on de un mensaje antes de conocer el valor de retorno del m´etodo llamado, emplearemos un await. La idea del await es paralizar la ejecuci´on del mensaje actual, permitiendo a otros mensajes del objeto ser ejecutados, y esperar a que 3.2. SEM ´ ANTICA 33 la variable futura de la llamada tenga un valor, es decir, que la llamada haya concluido. La construcci´on await tiene la siguiente sintaxis 1await o!f( args); y su tipo de retorno es el mismo que el del m´etodo de la llamada. El resto de la sintaxis de ABS empleada en este trabajo se reduce al uso de los if/else y del while, as´ı como de la declaraci´on de variables locales en los m´etodos y de asignaciones a variables de los resultados de la evaluaci´on de expresiones aritm´etico-l´ogicas. La sintaxis referente a estas construcciones del lenguaje son pr´acticamente similares a las de Java. El concepto de funci´on main en ABS lo cumple un conjunto de instrucciones ABS escritas entre llaves y situadas al final del archivo del c´odigo. 3.2. Sem´antica De forma similar al desarrollo expuesto para CABS, en esta secci´on seguiremos unos pasos similares para definir la sem´antica del lenguaje ABS. Un estado de un programa en ABS vendr´a representado por los objetos creados en ejecuci´on y por la informaci´on est´atica aportada por las clases e interfaces, es decir, el c´odigo de la implementaci´on de los m´etodos, tanto p´ublicos como privados, y la inicializaci´on de los atributos. Por tanto definimos StateABS como tuplas (O,C) donde el elemento O ser´a una lista de objetos instanciados y Ccontendr´a la definici´on de las clases e interfaces. Este ´ultimo elemento ser´a una lista de definiciones indexada por un identificador de clase. Contendr´a elementos de la forma (Inter, attrc, met, argsc) donde, en orden de izquierda a derecha, se tiene el nombre de interfaz que implementa una clase, los atributos o fields de la clase, los m´etodos que implementa junto con su definici´on (es decir, c´odigo y argumentos) y los argumentos de clase. Un objeto vendr´a dado a su vez por un identificador ´unico o, su nombre de clase, una cola de mensajes a la que llamaremos RT (Runtime tasks), un identificador de tarea que indique que mensaje est´a procesando el objeto en ese instante y la informaci´on del estado de los atributos mediante attr :Var ,→VABS, una funci´on que asigne a un nombre de variable un valor de ABS. Puesto que los identificadores de objetos pueden venir dados por un n´umero en Z, se puede ver que VABS es en esencia el mismo conjunto de valores que hemos definido para CABS. Por comodidad escogeremos esta opci´on. Es importante tener esto en cuenta puesto que, si us´aramos otro tipo de identificador para los objetos, ser´ıa necesario definir el conjunto de valores de ABS de otro modo y habr´ıa de tenerse en cuenta en el resto de argumentos formales que llevaremos a cabo que los valores en CABS no ser´ıan los mismos que en ABS. El papel de attr ser´a el mismo que ten´ıan los elementos de Loc en la sem´antica de CABS, permitiendo ahora tener objetos a los que se puede acceder usando un nombre de variable de Var. El concepto de tarea recoge la informaci´on del ´ambito local loc :Var ,→VABS, el c´odigo del m´etodo S∈StmABS y un identificador ´unico de tarea. Con esto quedan definidos 34 CAP´ ITULO 3. ABS: SINTAXIS Y SEM ´ ANTICA los elementos RT. No hay que confundir las variables de ´ambito local loc, declaradas dentro de un m´etodo, con los atributos del objeto attr que son un a˜nadido al contar con orientaci´on a objetos. Con estas definiciones b´asicas procedemos a dar una definici´on formal de la sem´antica de ABS. 3.2. SEM ´ ANTICA 35 3.2.1. Reglas de derivaci´on en ABS is local(x)is Int(x) [ass1 ABS] (O;(id, c, RT ;(loc, x =a;S, t), t, attr),C)→(O;(id, c, RT ;(loc hx7→ A JaKloc,attri, S, t), t, attr),C) is attr(x)is Int(x) [ass2 ABS] (O;(id, c, RT ;(loc, x =a;S, t), t, attr),C)→(O;(id, c, RT ;(loc, S, t), t, attr hx7→ A JaKloc,attri),C) Declint ABS(O;(id, c, RT ;(loc, Int x =a;S, t), t, attr),C)→(O;(id, c, RT ;(loc hx7→ A JaKloc,attri, S, t), t, attr),C) is local(x)is Bool(x) [ass3 ABS] (O;(id, c, RT ;(loc, x =b;S, t), t, attr),C)→(O;(id, c, RT ;(loc hx7→ B JbKloc,attri, S, t), t, attr),C) is attr(x)is Bool(x) [ass4 ABS] (O;(id, c, RT ;(loc, x =b;S, t), t, attr),C)→(O;(id, c, RT ;(loc, S, t), t, attr hx7→ B JbKloc,attri),C) Declbool ABS(O;(id, c, RT ;(loc, Bool x =b;S, t), t, attr),C)→(O;(id, c, RT ;(loc hx7→ B JbKloc,attri, S, t), t, attr),C) BJbKloc,attr =TRUE ifTRUE ABS (O;(id, c, RT ;(loc, if(b){S1}else{S2}S, t), t, attr),C)→(O;(id, c, RT ;(loc, S1S, t), t, attr),C) BJbKloc,attr =FALSE ifFALSE ABS (O;(id, c, RT ;(loc, if(b){S1}else{S2}S, t), t, attr),C)→(O;(id, c, RT ;(loc, S2S, t), t, attr),C) 36 CAP´ ITULO 3. ABS: SINTAXIS Y SEM ´ ANTICA [whileABS](O;(id, c, RT ;(loc, while(b){S1}S, t), t, attr),C)→(O;(id, c, RT ;(loc, if(b){S1while(b){S1}}S, t), t, attr),C) CJc0K= (Inter, attrc, met, argsc)check args(argsc, args) [objABS](O;(id, c, RT ;(loc, Inter inter =new c0(args); S, t), t, attr),C)→(O:o;(id, c, RT ;(loc [inter 7→ id0], S, t), t, attr),C) donde o= (id0, c0,[],⊥,attr0) con id0un nuevo identificador de objeto no utilizado y attr0=attrchargsc7→ E JargsKloc,attrilos atributos del nuevo objeto creado. La funci´on Eeval´ua los argumentos escogiendo entre AyBseg´un sea un entero o un booleano. loc ∪attr JinterK=id0CJc0K= (Inter, attrc, met, argsc)contains(met, m)check args(argsm, args) tskASYNC ABS (O;(id0, c0,RT0, t0,attr0)(id, c, RT ;(loc, inter!m(args); S, t), t, attr),C)→st donde tsk = (loc0, S0, t00) con t00 un identificador de tarea nuevo, loc0=nil [argsm7→ args] y met JmK= (S0, argsm) y el nuevo estado st = (O;(id0, c0,RT0:tsk, t0,attr0)(id, c, RT ;(loc, S, t), t, attr),C) loc ∪attr JintK=id0CJc0K= (Inter, attrc, met, argsc)contains(met, m)check args(argsm, args) tskSYNC ABS1(O;(id0, c0,RT0, t0,attr0)(id, c, RT ;(loc, Int x =await int!m(args); S, t), t, attr),C)→st donde o0= (id0, c0,RT0:tsk, t0,attr0), tsk = (loc0, S0, t00) con t00 un identificador de tarea nuevo y loc0=nil [argsm7→ args], met JmK= (S0, argsm) y st = (O;o0(id, c, RT ;(loc, Int x =await t0;S, t), t, attr),C) loc ∪attr JintK=id0CJc0K= (Inter, attrc, met, argsc)contains(met, m)check args(argsm, args) tskSYNC ABS2(O;(id0, c0,RT0, t0,attr0)(id, c, RT ;(loc, await int!m(args); S, t), t, attr),C)→st donde o0= (id0, c0,RT0:tsk, t0,attr0), tsk = (loc0, S0, t00) con t00 un identificador de tarea nuevo y loc0=nil [argsm7→ args], met JmK= (S0, argsm) y st = (O;o0(id, c, RT ;(loc, await t0;S, t), t, attr),C) tsk = (loc0, ε(ν), t00) [ret1 ABS](O;(id0, c0,RT0;tsk, t0,attr0)(id, c, RT ;(loc, Int x =await t0;S, t), t, attr),C)→st donde o0= (id0, c0,RT0, t0,attr0) y st = (O;o0(id, c, RT ;(loc [x7→ ν], S, t), t, attr),C) 3.2. SEM ´ ANTICA 37 tsk = (loc0, ε(ν), t00) [ret2 ABS](O;(id0, c0,RT0;tsk, t0,attr0)(id, c, RT ;(loc, await t0;S, t), t, attr),C)→(O;o0(id, c, RT ;(loc, S, t), t, attr),C) donde o0= (id0, c0,RT0, t0,attr0) tsk = (loc0, S, t00)S6=ε(ν) [waitABS](O;(id0, c0,RT0;tsk, t0,attr0)(id, c, RT ;(loc, Int x =await t0;S, t), t, attr),C)→st donde o0= (id0, c0,RT0, t0,attr0) y st = (O;o0(id, c, RT ;(loc, Int x =await t0;S, t),⊥,attr),C) [selecABS](O;(id, c, RT ;(loc, S, t),⊥,attr),C)→(O;(id, c, RT ;(loc, S, t), t, attr),C) [endABS](O;(id, c, RT ;(loc, return a;S, t), t, attr),C)→(O;(id, c, RT ;(loc, ε(AJaKloc,attr), t),⊥,attr),C) [deselecABS](O;(id, c, RT ;(loc, ε(ν), t), t, attr),C)→(O;(id, c, RT ;(loc, ε(ν), t),⊥,attr),C) 38 CAP´ ITULO 3. ABS: SINTAXIS Y SEM ´ ANTICA 3.3. Extensi´on sem´antica y sint´actica Adem´as de las definiciones anteriores asociadas al lenguaje ABS, puede resultar interesante a˜nadir una serie de estructuras auxiliares a modo de az´ucar sint´actico que puedan facilitarnos el camino en los siguientes cap´ıtulos de este trabajo. Es por ello por lo que hemos introducido en la sem´antica la notaci´on await t para indicar que esperamos a que termine la tarea con identificador ty que recuperamos su valor de retorno. Este tipo de construcci´on y otras m´as pueden no existir en el lenguaje original ABS, pero nosotros haremos uso de ellas como mera notaci´on para expresar el significado del resto de construcciones s´ı presentes en el lenguaje. 3.4. Ejemplos Sea el c´odigo en ABS 1module Cabs; 2import * from ABS . StdLib ; 3 4interface GLOBAL { 5Int getvar (); 6Unit setvar (Int val ); 7} 8class GlobalVariables () implements GLOBAL { 9Int var = 0; 10 11 Int getvar () { 12 return var; 13 } 14 15 Unit setvar (Int val ) { 16 var = val ; 17 } 18 } 19 20 interface Intf { 21 Unit f(Int value); 22 } 23 24 interface Intmain { 25 Int main (); 26 } 27 28 class Impf ( GLOBAL globalval ) implements Intf { 29 Unit f( Int value ) { 30 await globalval ! setvar ( value ); 3.4. EJEMPLOS 39 31 } 32 } 33 34 class Impmain ( GLOBAL globalval ) implements Intmain { 35 Int main () { 36 Intf funcf1 = new Impf ( globalval ); 37 funcf1 !f (1); 38 39 Intf funcf2 = new Impf ( globalval ); 40 funcf2 !f (2); 41 42 return 0; 43 } 44 } 45 46 { 47 GLOBAL globalval = new GlobalVariables (); 48 Intmain prog = new Impmain ( globalval ); 49 await prog !main (); 50 } Tras ejecutar el c´odigo de inicializaci´on, en el que creamos el objeto globaval e instanciamos un objeto que contiene la implementaci´on de main a la que llamamos con la instrucci´on await prog!main(); , nos encontramos en un estado ((0, GlobalV ariables, [],⊥,nil [var 7→ 0]) : (1, Impmain, (nil, S, 0),⊥,nil [globalval 7→ 0]),C) donde Ses el c´odigo de main. La tarea 0 del objeto 1 puede entrar a ejecutarse con la regla [selecABS] y podemos suponer que se ejecuta por completo, dando lugar por el camino a la creaci´on de dos objetos de la clase Impf, lo que nos lleva al estado ((0, GlobalV ariables, [],⊥,nil [var 7→ 0]) : (1, Impmain, (nil, (0),0),⊥,nil [globalval 7→ 0]) : (2, Impf, (nil [value 7→ 1] , S0,1),⊥,nil [globalval 7→ 0]) : (3, Impf, (nil [value 7→ 2] , S0,2),⊥,nil [globalval 7→ 0]),C) donde S0=await globalval!setvar(value); . En cualquier momento pueden ser seleccionadas las tareas 1 y 2 en sus respectivos objetos, creando dos tareas en el objeto 0, asociadas a cada una de las asignaciones sobre la variable global var. Llegando por ejemplo al estado ((0, GlobalV ariables, (nil [val 7→ 1] , S00,3) : (nil [val 7→ 2] , S00,4),⊥,nil [var 7→ 0]) : (1, Impmain, (nil, (0),0),⊥,nil [globalval 7→ 0]) : (2, Impf, (nil [value 7→ 1] , await 3,1),⊥,nil [globalval 7→ 0]) : (3, Impf, (nil [value 7→ 2] , await 4,2),⊥,nil [globalval 7→ 0]),C) 40 CAP´ ITULO 3. ABS: SINTAXIS Y SEM ´ ANTICA donde S00 es el c´odigo que asigna val al atributo var de la clase. Ahora la regla [selecABS] puede escoger alguna de las dos tareas del objeto 0. Es en este punto donde la selecci´on de tarea dar´a lugar a los dos entrelazamientos posibles del programa. Suponiendo que primero se ejecute la tarea 3 y posteriormente la tarea 4 se llega a ((0, GlobalV ariables, (nil [val 7→ 1] , ε, 3) : (nil [val 7→ 2] , ε, 4),⊥,nil [var 7→ 2]) : (1, Impmain, (nil, (0),0),⊥,nil [globalval 7→ 0]) : (2, Impf, (nil [value 7→ 1] , await 3,1),⊥,nil [globalval 7→ 0]) : (3, Impf, (nil [value 7→ 2] , await 4,2),⊥,nil [globalval 7→ 0]),C) En este momento los await de las tareas 1 y 2 pueden concluir y llegamos al estado final ((0, GlobalV ariables, (nil [val 7→ 1] , ε, 3) : (nil [val 7→ 2] , ε, 4),⊥,nil [var 7→ 2]) : (1, Impmain, (nil, (0),0),⊥,nil [globalval 7→ 0]) : (2, Impf, (nil [value 7→ 1] , ε, 1),⊥,nil [globalval 7→ 0]) : (3, Impf, (nil [value 7→ 2] , ε, 2),⊥,nil [globalval 7→ 0]),C) Cap´ıtulo 4 Traducci´on a ABS La traducci´on de CABS a ABS forma el grueso de este trabajo. La diferencia de paradigmas entre un lenguaje y otro hace que sea necesario la implementaci´on de algunas estructuras de datos adicionales ausentes en ABS. Adem´as de dichas estructuras, es necesario emplear algunos trucos para poder vencer las restricciones del lenguaje para crear el concepto de variable global o de llamada a funciones s´ıncrona. En este cap´ıtulo discutiremos este tema de una forma abstracta para posteriormente poder llevar a cabo la implementaci´on de un compilador correcto. 4.1. Variables globales y funciones La ausencia de memoria compartida entre los distintos COGs (Concurrent Object Group) o conjunto de tareas de un objeto hace que la idea de variable global no sea inmediata. Del mismo modo, es necesario discutir el concepto de funci´on al estilo de C, pese a que los m´etodos de una interfaz en ABS sean p´ublicos y a primera vista similares. Una primera aproximaci´on vendr´ıa dada por el uso de una ´unica clase en la que encapsular todo nuestro programa. Esta clase implementar´ıa una interfaz con todas las cabeceras de las funciones de nuestro programa. Adem´as contar´ıa entre sus atributos con las variables globales, consiguiendo de este modo una visibilidad completa desde cualquier punto del programa. Veamos qu´e ocurre con el siguiente c´odigo de ejemplo en CABS. En ´el se puede ver como se llama a la funci´on fcon thread haciendo que las dos asignaciones de la variable var1 puedan entrelazarse. 1int var1; 2 3void f() { 4var1 = 2; 41 48 CAP´ ITULO 4. TRADUCCI ´ ON A ABS 30 } Por ´ultimo, ser´ıa conveniente (y lo ser´a m´as adelante en la traducci´on de las funciones) tener un m´etodo que nos devuelva el array global para usarlo con algunos fines locales (concretamente el paso de arrays por referencia en los argumentos de una funci´on). Esto se consigue con un m´etodo retrieve que implemente la clase GlobalV ariables. Para el ejemplo anterior, quedar´ıa como 1interface GLOBAL { 2ArrayInt retrievearray (); 3Int getarray (Int indx ); 4Unit setarray (Int indx , Int val); 5Unit init (); 6} 7 8class GlobalVariables () implements GLOBAL { 9... 10 ArrayInt retrievearray () { 11 return array; 12 } 13 ... 14 } 15 ... No hay que decir que las clases que hemos implementado en esta secci´on permiten su uso en cualquier ´ambito local de un m´etodo, con lo que tambi´en contaremos con arrays locales en ABS. 4.2.1. Arrays multidimensionales El lenguaje CABS permite en su sintaxis declarar arrays multidimensionales al estilo de C. ABS no cuenta con un tipo de datos similar, pero, gracias a la propuesta previamente expuesta, podemos simular el comportamiento de las matrices estableciendo una biyecci´on con la representaci´on de un array de tama˜no el producto de los tama˜nos de las dimensiones de la matriz. En otras palabras, la traducci´on implementada en este trabajo considera las matrices como un array unidimensional. A modo de explicaci´on, sea mat una matriz multidimensional entera en intN1×· · ·×intND y supongamos que queremos acceder a la posici´on (i1, . . . , iD) donde ∀j∈ {1, . . . , D} tenemos ij∈ {0, . . . , Nj−1}, entonces la posici´on pcorrespondiente a dicho elemento en un array en intQD i=1 Nivendr´ıa dada por p=PD l=1 il·(Ql−1 j=1 Nj). 4.3. Expresiones aritm´eticas CABS presenta una gran flexibilidad en sus expresiones aritm´etico-l´ogicas no presentes en ABS. La sintaxis de ABS obliga a que el valor de retorno devuelto por una funci´on solo 4.3. EXPRESIONES ARITM ´ ETICAS 49 pueda ser asignado a una variable, no pudiendo ser usado inmediatamente en una expresi´on del mismo tipo que el de retorno. Esto nos obliga a traducir las expresiones aritm´eticas en una serie de asignaciones auxiliares cuyas variables posteriormente se operan con los valores almacenados en ellas. Ser´a por tanto necesario tener un modo de obtener nombres de variables auxiliares que no se referencien en ning´un otro punto del programa traducido. Sea por tanto Aux :N→Var una funci´on definida sobre los enteros que devuelve el n-´esimo nombre de variable libre. En un sentido estricto esta funci´on deber´ıa tomar como argumento el programa en CABS y la traducci´on parcial en ABS para saber qu´e nombres de variable han sido ya usados. A modo de simplificaci´on podemos evitar esto reservando un conjunto de nombres de variables para este prop´osito que no sean accesibles al usuario. Esta es la idea que posteriormente se llevar´a a cabo en la implementaci´on del compilador. De ahora en adelante nos referiremos a este conjunto como VarR⊂Var. Un posible ejemplo de subconjunto VarRpodr´ıa ser {aux var v :v∈N}, que por tener la misma cardinalidad que Nnos permite crear una biyecci´on inmediata. Teniendo esto en cuenta, resulta f´acil pensar en definir la traducci´on de las expresiones como una funci´on que toma una expresi´on en CABS junto con un natural vy que devuelve una expresi´on en ABS junto con un natural que indique el siguiente natural no utilizado en la traducci´on. Si garantizamos no repetir un mismo npara dos expresiones distintas entonces garantizamos que las variables auxiliares no son usadas m´as all´a de una ´unica asignaci´on y una ´unica referencia. Especificamos esta idea con la definici´on de las funciones CAexp :Aexp →N→(ABS×N) y su hom´ologa CBexp para las expresiones booleanas: CAexp JnKv= (Int (Aux v) = n, v + 1) CAexp JxKv= (Int (Aux v) = x, v + 1) donde xes variable entera local. CAexp JxKv= (Int (Aux v) = await globalval!getx(), v + 1) donde xes variable entera global. CAexp Ja1Aa2Kv= (c1;c2;Int (Aux v00)=(Aux (v0−1)) A(Aux (v00 −1)), v00 + 1) donde CAexp Ja1Kv= (c1, v0) y CAexp Ja2Kv0= (c2, v00) CBexp JfalseKv= (Bool (Aux v) = False, v + 1) CBexp JtrueKv= (Bool (Aux v) = True, v + 1) CBexp JxKv= (Bool (Aux v) = x, v + 1) donde xes variable booleana local. CBexp JxKv= (Bool (Aux v) = await globalval!getx(), v + 1) donde xes variable booleana global. CBexp Jb1Bb2Kv= (c1;c2;Bool (Aux v00) = (Aux (v0−1)) B(Aux (v00 −1)), v00 + 1) donde CBexp Jb1Kv= (c1, v0) y CBexp Jb2Kv0= (c2, v00) CBexp Ja1a2Kv= (c1;c2;Bool (Aux v00) = (Aux (v0−1)) (Aux (v00 −1)), v00 + 1) donde CAexp Ja1Kv= (c1, v0) y CAexp Ja2Kv0= (c2, v00) y comparador. Para las llamadas a funciones supondremos por el momento que las interfaces y clases asociadas se encuentran traducidas en alg´un otro punto del c´odigo y que por tanto podemos 50 CAP´ ITULO 4. TRADUCCI ´ ON A ABS hacer uso de sus nombres. CAexp Jf(e1. . . en)Kv1= (c1. . . cn Intf(Aux (vn+1)) = new Impf(globalval) Int (Aux (vn+1 + 1)) = (Aux (vn+1))!((Aux (v2−1)),..., (Aux (vn+1 −1))), vn+1 + 2) donde CExp JeiKvi= (ci, vi+1) (escogiendo CAexp oCBexp seg´un convenga) CBexp Jf(e1. . . en)Kv1= (c1. . . cn Intf(Aux (vn+1)) = new Impf(globalval) Bool (Aux (vn+1 + 1)) = (Aux (vn+1))!((Aux (v2−1)),..., (Aux (vn+1 −1))), vn+1 + 2) donde CExp JeiKvi= (ci, vi+1) (escogiendo CAexp oCBexp seg´un convenga) 4.4. Traducci´on de c´odigo Tras esta introducci´on, podemos vislumbrar qu´e aspecto tendr´a la traducci´on de c´odigo llevada a cabo en este trabajo. Obviaremos el pre´ambulo de los programas ABS, que incluir´a la definici´on de los clases Array, y nos centraremos en otros aspectos m´as importantes. Sea pues la funci´on C:CABS →N→(ABS ×N) nuestra funci´on de traducci´on de CABS a ABS definida recursivamente del siguiente modo: CJint var;Kv= (Int var, v) CJbool var;Kv= (Bool var, v) CJvar =a;Kv= (c;var = (Aux (v0−1)), v0) donde CAexp JaKv= (c, v0) y var variable local entera CJvar =b;Kv= (c;var = (Aux (v0−1)), v0) donde CBexp JbKv= (c, v0) y var variable local booleana CJvar =a;Kv= (c;await globalval!setvar(Aux (v0−1)), v0) donde CAexp JaKv= (c, v0) y var variable global entera CJvar =b;Kv= (c;await globalval!setvar(Aux (v0−1)), v0) donde CBexp JbKv= (c, v0) y var variable global booleana CJS1S2Kv= (c1c2, v00) donde CJS1Kv= (c1, v0) y CJS2Kv0= (c2, v00) CJif(b){S1}else{S2}Kv= (c1;if(Aux (v0−1)){c2}else{c3}, v000) donde CBexp JbKv= (c1, v0), CJS1Kv0= (c2, v00) y CJS2Kv00 = (c3, v000) CJwhile(b){S}Kv= (c1;while(Aux (v0−1)){c2c3Aux (v0−1) = Aux (v000 −1); }, v000) donde CBexp JbKv= (c1, v0), CJSKv0= (c2, v00) y CBexp JbKv00 = (c3, v000) 4.4. TRADUCCI ´ ON DE C ´ ODIGO 51 Sobre la traducci´on del while cabe destacar que es necesario traducir dos veces su condici´on y el uso de una asignaci´on adicional. Esto es debido a que el concepto de while obliga a evaluar su condici´on antes de la ejecuci´on de su cuerpo en cada una de las iteraciones para decidir si el salto se toma o no. Por el modo en que se han traducido las expresiones aritm´etico-l´ogicas, la condici´on en ABS de un while se reduce a comprobar el valor asignado a una variable auxiliar y es por esto por lo que, sobre dicha variable, se har´a una asignaci´on adicional al final de toda iteraci´on. En segundo lugar, hace falta mencionar que las funciones de traducci´on de expresiones booleanas no contemplan la reutilizaci´on de variables, por lo que aunque la condici´on sea la misma, se emplear´an unos nombres de variables nuevos al final del cuerpo del while respecto a los que se usaban al evaluar la condici´on fuera del cuerpo. A efectos pr´acticos, es f´acil demostrar que los nombres de las variables auxiliares no influyen en el c´omputo de la expresi´on booleana. De hecho se ve claramente que la traducci´on es la misma salvo un offset en el natural que identifica a las variables auxiliares. Es por esto por lo que podemos entender que en la traducci´on del c´odigo se puede indistintamente sustituir el c´odigo c3por c2en la regla del while si por motivos de simplicidad hiciera falta a la hora de desarrollar la correcci´on de esta traducci´on. En una implementaci´on real esto no es inmediato porque los compiladores o interpretes de ABS no permiten la declaraci´on duplicada de variables, problema que en este trabajo no nos ata˜ne a nivel abstracto. Para la traducci´on de las funciones necesitamos previamente una traducci´on de los argumentos Carg :Args →ArgsABS que en esencia lo ´unico que hace es cambiar los tipos de CABS a los de ABS. Carg ε=ε Carg (int var, arg) = Int var, Carg arg Carg (bool var, arg) = Bool var, Carg arg Usando esta traducci´on de argumentos tenemos que CJint func(arg){Sreturn a}Kv= (interface Intfunc{Int func(Carg arg); } class Impfunc(GLOBAL globalval) implements Intfunc{ Int func(Carg arg){c c0return Aux (v00 −1)}}, v00) donde CJSKv= (c, v0) y CAexp JaKv0= (c0, v00) CJbool func(arg){Sreturn b}Kv= (interface Intfunc{Bool func(Carg arg); } class Impfunc(GLOBAL globalval) implements Intfunc{ Bool func(Carg arg){c c0return Aux (v00 −1)}}, v00) donde CJSKv= (c, v0) y CBexp JbKv0= (c0, v00) CJvoid func(arg){S}Kv= (interface Intfunc{Unit func(Carg arg); } class Impfunc(GLOBAL globalval) implements Intfunc{ Unit func(Carg arg){c}}, v0) donde CJSKv= (c, v0) 52 CAP´ ITULO 4. TRADUCCI ´ ON A ABS y para las variables globales tenemos CJvar =a;Kv= (c;await globalval!setvar(Aux (v0−1)), v0) donde CAexp JaKv= (c, v0) y var variable global entera CJvar =b;Kv= (c;await globalval!setvar(Aux (v0−1)), v0) donde CBexp JbKv= (c, v0) y var variable global booleana Por ´ultimo, hablaremos de la traducci´on del thread. Como ya hemos comentado en las secciones anteriores, la traducci´on propuesta es similar a la de las llamadas a funci´on con la diferencia de que no se espera a la resoluci´on del valor futuro de retorno. Su regla es CJthreadf(e1. . . en)Kv1= (c1. . . cn Intf(Aux (vn+1)) = new Impf(globalval) (Aux (vn+1))!((Aux (v2−1)),...,(Aux (vn+1 −1))), vn+1 + 1) donde CExp JeiKvi= (ci, vi+1) (escogiendo CAexp oCBexp seg´un convenga) 4.4.1. Traducci´on de arrays Como comentamos ya en el cap´ıtulo sobre la sem´antica de CABS, los arrays quedar´an excluidos de la demostraci´on formal y es por ello por lo que hemos decidido no incluirlos en la definici´on de la traducci´on. No obstante, la implementaci´on s´ı los tiene en cuenta y lleva a cabo la compilaci´on teniendo en cuenta lo comentado en la secci´on sobre arrays de este cap´ıtulo. Cap´ıtulo 5 Correcci´on A lo largo de este cap´ıtulo usaremos las definiciones de las sem´anticas previamente expuestas para comprobar que la traducci´on propuesta de CABS a ABS es correcta. En otras palabras, durante las pr´oximas secciones, demostraremos que dado un c´odigo en CABS y partiendo de un estado inicial podemos “ejecutar” una serie de pasos hasta llegar a un nuevo estado que tiene un hom´ologo en ABS y que resulta de ejecutar la traducci´on desde un estado equivalente al inicial en CABS (y viceversa). Este procedimiento es conocido como bisimulaci´on y nos permitir´a hacer afirmaciones tan fuertes como las que buscamos, es decir, que si tenemos un c´odigo en CABS y dada su traducci´on sabemos, usando la herramientas ya desarrolladas para ABS, que cumple una cierta propiedad partiendo de un estado, sabremos entonces que el mismo resultado se sostiene para el c´odigo en CABS. 5.1. Equivalencia entre estados Sea (G,F,RP) un estado en CABS y (O,C) un estado en ABS. Diremos que estos estados son equivalentes si: dado (id, c, RT, t, attr)∈Oel objeto correspondiente a la clase GlobalVariables, tenemos que las funciones Gyattr son la misma. para todo nombre de funci´on func con F(func)=(t, S, args, a), tenemos que CJImpfuncK= (Intfunc,nil, met, argc) donde met JfuncKcontiene la traducci´on de los argumentos args y del c´odigo de la funci´on y los argumentos de clase argc contienen solo una variable con el tipo de la interfaz de las variables globales. cada elemento en RP se corresponde con un conjunto de tareas en los objetos de O, en concreto, cada entorno de variables apilado se corresponde con los atributos (obviando variables auxiliares) de una tarea cuyo c´odigo traducido se corresponde con un segmento de instrucciones del c´odigo del proceso. Lo que se quiere decir con esto es que, mientras que las llamadas a funci´on en CABS se corresponden con el apilamiento de un nuevo entorno de variables y la concatenaci´on del c´odigo de la funci´on con el c´odigo actual del proceso, en ABS se crea una nueva tarea a la que se espera para obtener el valor de retorno. 53 54 CAP´ ITULO 5. CORRECCI ´ ON en caso de existir un elemento (local :s, x =e;S)∈RP donde etiene elementos en Vya calculados, se tiene que en la tarea del estado equivalente se han ejecutado ya las asignaciones a las variables auxiliares correspondientes con los valores ya calculados y, por tanto, quedan por calcular las asignaciones a variables auxiliares restantes en la expresi´on. En otras palabras, cada paso de evaluaci´on de una expresi´on ser´a una asignaci´on en la traducci´on en ABS. Esto es v´alido tanto para enteros como para booleanos. 5.2. Correcci´on de las expresiones aritm´etico-l´ogicas Una de las peculiaridades que tiene CABS, es permitir en sus expresiones una notaci´on para realizar llamadas a funci´on con retorno de valor. Como ya notamos en el cap´ıtulo anterior, esto hace que la traducci´on se apoye en el uso de unas variables auxiliares que permiten dividir el c´omputo de una expresi´on en el c´omputo de las distintas subexpresiones que la componen. Cada expresi´on utilizada en un programa CABS se corresponde de forma un´ıvoca con una variable auxiliar en ABS que almacenar´a el valor de la expresi´on cuando este est´e disponible. De este modo, en todo momento podemos hacer uso de esta informaci´on, aunque, por simplificar la notaci´on, no est´e presente en el estado del programa. Hecha esta introducci´on, procedemos a comprobar en primer lugar que las asignaciones hechas en CABS se corresponden con las de la traducci´on de estas a ABS, llegando de estados equivalentes a estados equivalentes en un solo paso. En esta memoria expondremos solo el proceso para las expresiones aritm´eticas. El caso de las expresiones booleanas es completamente an´alogo salvo tipo y operadores empleados. 5.2.1. Variables locales Caso x=νcon ν∈V Sean (G,F,RP ;(local :s, x =ν;S)) y (O;(id, c, RT ;(loc, x =aux var k;SABS, t), t, attr),C) estados equivalentes, donde la variable auxiliar k-´esima es la variable asignada a la expresi´on νde forma que loc(aux var k) = ν. Tenemos que del estado (G,F,RP ;(local :s, x =ν;S)), aplicando la regla [ass2 C], llegamos al estado (G,F,RP ;(local [x7→ ν] : s, S)) en CABS. Por otro lado, del estado equivalente en ABS (O;(id, c, RT ;(loc, x =aux var k;S, t), t, attr),C), aplicando la regla de asignaci´on local correspondiente, llegamos al estado (O;(id, c, RT ; (loc hx7→ A Jaux var kKloc,attri, SABS, t), t, attr),C) y del hecho de que dicha variable auxiliar tenga el valor de νllegamos inmediatamente a un estado equivalente. 5.2. CORRECCI ´ ON DE LAS EXPRESIONES ARITM ´ ETICO-L ´ OGICAS 55 Caso x=n Sea (G,F,RP ;(local :s, x =n;S)) y sea (O;(id, c, RT ;(loc, Int aux var k = n;x=aux var k;SABS, t), t, attr),C) su estado equivalente, donde la variable auxiliar k-´esima es la variable asignada a la expresi´on n. En este caso, solo podemos aplicar para el proceso actual la regla [ass1 C] que delega la acci´on en las reglas para expresiones aritm´etico-l´ogicas. La regla aplicable en esta situaci´on es [numA] con lo que llegamos al estado (G,F,RP ;(local :s, x =NJnK;S)). En el lado de ABS aplicamos la regla de asignaci´on sobre la variable auxiliar llegando al estado (O;(id, c, RT ;(loc haux var k 7→ A JnKloc,attri, x =aux var k;SABS, t), t, attr),C) preserv´andose la equivalencia entre estados al asignar el valor de la expresi´on a su variable auxiliar. Caso x=f() (simplificaci´on sin argumentos) Sean los estados equivalentes (G,F,RP ;(local :s, x =f(); S)) y (O;(id, c, RT ; (loc, Intf aux var (k−1) = new Impf(globalval); Int aux var k =await auxi var (k− 1)!f(); x=aux var k;SABS, t), t, attr),C) donde la variable auxiliar k-´esima es la variable asignada a la expresi´on f(). La sem´antica de CABS nos permite usar la regla [ass1 C] con la regla call2 Aresultando en el estado (G,F,RP ;(nil :local :s, SFx=UNSTACK (a) ; S)) donde aes la expresi´on de retorno de f. Por otro lado, en la sem´antica de ABS, podemos aplicar primero la regla de creaci´on de objetos y a continuaci´on la regla de llamada s´ıncrona, resultando el estado (O;(id0, c0,(nil, SF ABS, t0),⊥,attr0) (id, c, RT ;(loc, Int aux var k =await t0;x=aux var k;SABS, t), t, attr),C) Llegados a este punto tenemos un estado que es equivalente al resultante en la sem´antica de CABS puesto que el concepto de apilar un nuevo ´ambito de variables en ABS se ve reflejado creando un objeto nuevo que tiene como ´unica tarea asignada el c´omputo del c´odigo traducido de la funci´on f. El objeto original se ve pausado por el await hasta que no termine de ejecutarse el c´odigo de f, imitando el concepto del c´odigo concatenado en CABS que no deja ejecutar el resto de instrucciones hasta no terminar con las de la funci´on. Otro detalle a tener en cuenta es el indicador de tarea actual. Tras dar los dos pasos anteriores en la sem´antica de ABS se nos lleva a tener como tarea asignada en el nuevo objeto a ⊥. Evidentemente, antes de poderse ejecutar la primera instrucci´on de fes necesario que se ejecute la regla de selecci´on de tarea. El hecho de que ning´un objeto de nuestra traducci´on vaya a ejecutar m´as de una tarea (a excepci´on del objeto de variables globales del que hablaremos m´as adelante) nos permite extender la idea de equivalencia a este estado actual, puesto que consideramos que aplicar una regla de selecci´on no afecta en esencia a la configuraci´on actual en ABS ya que solo lo hacen los “movimientos” en el 56 CAP´ ITULO 5. CORRECCI ´ ON c´odigo. De forma similar, el hecho de tener que dar dos pasos tampoco afecta, pese a existir una concurrencia en la sem´antica. El motivo es que entre ambos pasos el objeto creado solo es referenciado por una variable auxiliar de modo que se garantiza que no puede ser modificado desde ning´un otro punto de la ejecuci´on. De este modo podemos volver a extender el concepto de equivalencia permitiendo que el paso intermedio de creaci´on del objeto (omitido en este texto) pueda ser tambi´en considerado un estado que mantiene la equivalencia con (G,F,RP ;(nil :local :s, SFx=UNSTACK (a) ; S)). Con esto se quiere decir que, al igual que las reglas de selecci´on de tarea, la creaci´on de objetos no altera tampoco el estado intr´ınseco del programa. Caso x=UNSTACK (ν)con ν∈V Sean los estados equivalentes (G,F,RP ;(local0:local :s, x =UNSTACK (ν) ; S)) y (O;(id0, c0,(loc0,return aux var k0, t0), t0,attr0) (id, c, RT ;(loc, Int aux var k =await t0;x=aux var k;SABS, t), t, attr),C) donde la variable auxiliar k0-´esima es la variable asignada a la expresi´on ν, que tiene su valor asignado en loc0, y la k-´esima al unstack. En el caso de CABS, aplicar la regla [ass1 C] con la regla unstack2 Apara la expresi´on nos lleva al estado (G,F,RP ;(local :s, x =ν;S)). En el caso de ABS, podemos aplicar la regla de retorno que nos lleva a un estado intermedio (O;(id0, c0,(loc0, ε(AJaux var k0Kloc,attr), t0), t0,attr0) (id, c, RT ;(loc, Int aux var k =await t0;x=aux var k;SABS, t), t, attr),C) Desde este estado se puede aplicar la regla del await que permite recoger el valor de νy asign´arselo, en este caso, a la variable aux var k, llegando al estado (O;(id0, c0,[],⊥,attr0) (id, c, RT ;(loc [aux var k 7→ ν], x =aux var k;SABS, t), t, attr),C) que mantiene la equivalencia. De nuevo se nos presenta la discusi´on de los pasos m´ultiples. El mismo argumento que hemos presentado anteriormente es aplicable a esta situaci´on y podemos extender la equivalencia de estados a los estados intermedios por los que se pasa en la sem´antica de ABS para llevar a cabo el return. Cabe destacar que el concepto de desapilar un entorno en CABS queda reflejado en el hecho de que el objeto con el ´ambito superior no vuelve a ser usado y queda vac´ıo de tareas. 5.2. CORRECCI ´ ON DE LAS EXPRESIONES ARITM ´ ETICO-L ´ OGICAS 57 Caso x=a1a2 Antes de discutir este caso conviene ver que en CABS el c´omputo de a1a2precisa del c´omputo de a1, de modo que el argumento que vamos a seguir para el caso compuesto es asumir que todo va bien si nos encontr´aramos con la expresi´on a1y que por tanto la asunci´on se puede emplear para la expresi´on a1a2. Otro detalle importante a tener en cuenta es que no se empieza a procesar la expresi´on a2hasta que no hemos completado el c´omputo de a1, como se refleja en las reglas de la sem´antica de CABS. Esto se reflejar´a tambi´en en ABS ya que las asignaciones de la expresi´on a2vienen precedidas por las de la expresi´on a1. Dicho esto, sean los estados equivalentes (G,F,RP ;(local :s, x =a1a2;S)) y (O;(id, c, RT ;(loc, c1c2Int aux var k =aux var k1aux var k2; x=aux var k;SABS, t), t, attr),C) donde c1es el c´odigo asociado a a1,c2el asociado a a2yaux var k1,aux var k2y aux var k las variables asociadas a cada una de las expresiones aritm´eticas en juego. En concreto tenemos que la ´ultima instrucci´on de c1, por el modo en que hemos definido la traducci´on, se corresponde con una asignaci´on a su variable auxiliar. Por el modo en que est´an definidas las expresiones aritm´eticas, podemos aplicar inducci´on estructural con lo que, por hip´otesis de inducci´on tenemos que los estados equivalentes (G,F,RP ; (local :s, x =a1;S)) y (O;(id, c, RT ;(loc, c1x=aux var k1;SABS, t), t, attr),C) llegan en un solo paso a los estados equivalentes (G,F,RP ;(local :s, x =a0 1;S)) y (O;(id, c, RT ;(loc, c0 1x=aux var k1;SABS, t), t, attr),C). Teniendo en cuenta esto y que si tenemos un c´odigo en ABS, S1, que en un paso desde un estado dado al que denotaremos por sse llega a un estado s0con c´odigo S0 1entonces tendr´ıamos un comportamiento similar con el c´odigo S1S2yS0 1S2(en otras palabras, el concatenar c´odigo por detr´as no altera el significado de los estados intermedios), llegamos a que de los estados originales llegamos en un paso a los estados (G,F,RP ;(local : s, x =a0 1a2;S)) y (O;(id, c, RT ;(loc, c0 1c2Int aux var k =aux var k1aux var k2; x=aux var k;SABS, t), t, attr),C) que son equivalentes. Casos x=νa2yx=νµcon ν, µ ∈Z La situaci´on del primer caso es completamente an´aloga a la del caso anterior con la diferencia de que la hip´otesis de inducci´on es aplicada sobre la expresi´on a2. Para el segundo caso tenemos los estados equivalentes (G,F,RP ;(local :s, x = νµ;S)) y (O;(id, c, RT ;(loc, Int aux var k =aux var k1aux var k2;x= 64 CAP´ ITULO 6. IMPLEMENTACI ´ ON: COMPILADOR DE CABS A ABS •An´alisis l´exico: a partir del c´odigo de origen se extraen los distintos elementos l´exicos o tokens que lo componen, por ejemplo, las palabras reservadas del lenguaje, los nombres de variables, etc. •An´alisis sint´actico: usando los token del an´alisis l´exico, mediante el uso de un aut´omata determinista que reconozca la gram´atica del lenguaje, se crea un ´arbol de sintaxis abstracta en cuyos nodos podemos encontrar las piezas l´ogicas que componen nuestro programa, por ejemplo, las asignaciones de variables, la declaraci´on de funciones, etc. •An´alisis est´atico: en esta fase se analizan los identificadores usados en el programa, en busca de usos il´ıcitos como en el caso de las asignaciones en variables no declaradas, y los tipos de las expresiones que permiten descartar programas con errores. De este proceso se obtiene una tabla de s´ımbolos que puede ser de ayuda en la traducci´on final del c´odigo. Back-end o fase de traducci´on: a partir del ´arbol de sintaxis abstracta y del resto de estructuras obtenidas en la etapa anterior, el compilador genera un c´odigo objeto entendible para la m´aquina o interprete para el que est´a destinado. En esta etapa tambi´en se pueden llevar a cabo algunas optimizaciones, pero hablar de ello no es nuestro objetivo. 6.2. JLex JLex1es un generador de analizadores l´exicos en java desarrollado en la Universidad de Princeton. A partir de una especificaci´on de los tokens de un lenguaje, JLex genera un aut´omata capaz de reconocerlos recogido en una clase de Java. El aut´omata empleado en los analizadores l´exicos es un aut´omata finito determinista, categor´ıa en la que se encuentran los reconocedores de los lenguajes formales m´as b´asicos conocidos como lenguajes regulares. La especificaci´on del analizador l´exico de CABS se puede encontrar en el archivo parser.lex dentro del paquete parser. A su vez, dentro de este paquete se encuentran la clase Yytoken, que ser´a el tipo de objeto manipulado por el analizador sint´actico, y el archivo Yylex.java, con las clases asociadas al aut´omata finito determinista. 6.3. CUP CUP2(Construction of Useful Parsers) es un generador de analizadores sint´acticos LALR(1) desarrollado en Java y mantenido por la Universidad T´ecnica de Munich (TUM). 1https://www.cs.princeton.edu/~appel/modern/java/JLex/current/manual.html 2http://www2.cs.tum.edu/projects/cup/ 6.3. CUP 65 Figura 6.1: Captura de las reglas para la generaci´on del lexer. Figura 6.2: Captura de las reglas de la gram´atica de CABS. 66 CAP´ ITULO 6. IMPLEMENTACI ´ ON: COMPILADOR DE CABS A ABS Con una sintaxis similar a la de YACC, se puede especificar la gram´atica del lenguaje para el que uno quiere crear un parser y CUP genera un analizador recogido en una clase de java. La gram´atica de CABS se encuentra en el fichero synt.cup dentro del paquete parser. La clase parser, contenida tambi´en en el paquete anterior, es el archivo generado por CUP. 6.4. Estructura del compilador El analizador sint´actico se apoya en gran medida en la estructura de nodos que el desarrollador del lenguaje determina para su creaci´on. Puesto que tras la fase de parser se obtiene un primer ´arbol de sintaxis abstracta, es necesario ya para esta fase conocer cu´ales son las clases empleadas para este prop´osito. La jerarqu´ıa de los nodos empleados en CABS se divide en los siguientes paquetes: ControlStructures: contiene los bloques asociados a las estructuras de decisi´on como son los condicionales (IfNode) y lo bucles (LoopNode). Expressions: contiene los nodos del ´arbol de sintaxis abstracta asociados a las expresiones aritm´etico-l´ogicas. Las clases pertenecientes a este paquete son las asociadas a los enteros y booleanos (NumNode y BoolNode respectivamente), los operadores (OperatorNode), las expresiones binarias de dos operandos y un operador (BinaryExpression) y unarias de un operando y un operador (UnaryExpression). Functions: paquete formado con todas las clases asociadas a la declaraci´on de funciones y procedimientos y sus llamadas, incluidas las de creaci´on de un nuevo hilo. Variables: paquete compuesto por las clases empleadas en la declaraci´on de variables y arrays y su uso en asignaciones y expresiones aritm´etico-l´ogicas. Adem´as de estos nodos, existen otros nodos m´as generales que permiten completar los ´arboles de sintaxis abstracta con el resto de construcciones t´ıpicas de un lenguaje de programaci´on. Algunos de estos nodos son las asignaciones (AssNode), los bloques de c´odigo (BlockNode y GlobalBlockNode) o los tipos de retorno y de variables (TypeNode). La construcci´on del ´arbol de derivaci´on se hace recursivamente, aprovechando la recursi´on propia de los analizadores sint´acticos LALR. Posteriormente, el control del resto de fases es retomado por la clase Manager, que se encarga de iniciar los sucesivos recorridos del ´arbol para inicializar las tablas de identificadores de s´ımbolos, es decir, asociar a cada uso de una variable o funci´on su declaraci´on, y realizar la comprobaci´on de tipos y la existencia de la funci´on main. Por ´ultimo, si llegados a este punto no hay ning´un error de compilaci´on, se procede a la generaci´on de c´odigo, para lo cual, cada nodo cuenta con un m´etodo de traducci´on que propaga la llamada recursivamente a los nodos de los que depende. De este modo, 6.4. ESTRUCTURA DEL COMPILADOR 67 aprovechando la estructura del ´arbol, se escribe de forma ordenada en un archivo las instrucciones del c´odigo destino. 68 CAP´ ITULO 6. IMPLEMENTACI ´ ON: COMPILADOR DE CABS A ABS Cap´ıtulo 7 SYCO: SYstematic testing tool for Concurrent Objects SYCO es una de las herramientas implementadas sobre el lenguaje ABS que permite el testing de programas concurrentes escritos en este lenguaje. La idea de SYCO es que, a partir del c´odigo de un programa, el programador pueda saber de antemano las posibles ejecuciones del programa adem´as de conocer si el programa presenta posibles situaciones de deadlock. El n´ucleo de SYCO incluye implementaciones de t´ecnicas de partial-order reduction que permiten la evaluaci´on de ramas redundantes como las que se nos han presentado al principio de este trabajo en algunos ejemplos. A trav´es de una interfaz web, uno puede obtener visualmente el resultado que SYCO genera sobre el c´odigo proporcionado. Veamos algunos ejemplos de uso sobre el c´odigo ABS generado a partir de un c´odigo en CABS. 1int var; 2 3int main () { 4thread f(1); 5thread f(2); 6return 0; 7} 8 9void f(int value ) { 10 var = value ; 11 } En este ejemplo tenemos que la funci´on main lanza dos hilos que ejecutar´an la funci´on f dando como posibles resultados finales var = 1 y var = 2. La traducci´on a ABS quedar´ıa, resumiendo parte de la traducci´on que no es necesaria para este ejemplo, como: 69 70CAP´ ITULO 7. SYCO: SYSTEMATIC TESTING TOOL FOR CONCURRENT OBJECTS 1module Cabs; 2import * from ABS . StdLib ; 3 4interface GLOBAL { 5Int getvar (); 6Unit setvar (Int val ); 7Unit initialize (); 8} 9 10 class GlobalVariables () implements GLOBAL { 11 Int var = 0; 12 Unit initialize () { 13 } 14 Int getvar () { 15 return var; 16 } 17 Unit setvar (Int val ) { 18 var = val ; 19 } 20 } 21 22 interface Intf { 23 Unit f(Int value); 24 } 25 interface Intmain { 26 Int main (); 27 } 28 29 class Impf ( GLOBAL globalval ) implements Intf { 30 Unit f( Int value ) { 31 await globalval ! setvar ( value ); 32 } 33 } 34 35 class Impmain ( GLOBAL globalval ) implements Intmain { 36 Int main () { 37 Intf aux_var_0 = new Impf ( globalval ); 38 Int aux_var_1 = 1; 39 aux_var_0 !f( aux_var_1 ); 40 Intf aux_var_2 = new Impf ( globalval ); 41 Int aux_var_3 = 2; 42 aux_var_2 !f( aux_var_3 ); 43 Int aux_var_4 = 0; 44 return aux_var_4 ; 45 } 46 } 71 47 48 { 49 GLOBAL globalval = new GlobalVariables (); 50 await globalval ! initialize (); 51 Intmain prog = new Impmain ( globalval ); 52 await prog !main (); 53 } Y el resultado que nos proporciona la herramienta SYCO es: Independence constraints generated in 908 ms. Number of executions: 2 Total time: 5 Total number of states explored during 2 executions: 16 Total number of tasks executed during 2 executions: 7 Execution 1, number of tasks: 6 (Click here to see the sequence diagram) - State: |------object(1,’GlobalVariables’,[field(var,2)]) |------object(2,’Impmain’,[field(globalval,ref(1))]) |------object(3,’Impf’,[field(globalval,ref(1))]) |------object(4,’Impf’,[field(globalval,ref(1))]) |------object(main,main,[]) - Trace: |------’Time: 0, Object: main, Task: 0:main’ |------’Time: 1, Object: GlobalVariables_1, Task: 1:initialize’ |------’Time: 2, Object: 0:main(54), Task: 0:main(54)’ |------’Time: 3, Object: Impmain_2, Task: 3:main’ |------’Time: 4, Object: 0:main(56), Task: 0:main(56)’ |------’Time: 5, Object: Impf_3, Task: 5:f’ |------’Time: 6, Object: GlobalVariables_1, Task: 7:setvar’ |------’Time: 7, Object: Impf_3, Task: 5:f(34)’ |------’Time: 8, Object: Impf_4, Task: 6:f’ |------’Time: 9, Object: GlobalVariables_1, Task: 9:setvar’ |------’Time: 10, Object: Impf_4, Task: 6:f(34)’ Execution 2, number of tasks: 6 (Click here to see the sequence diagram) - State: |------object(1,’GlobalVariables’,[field(var,1)]) |------object(2,’Impmain’,[field(globalval,ref(1))]) |------object(3,’Impf’,[field(globalval,ref(1))]) |------object(4,’Impf’,[field(globalval,ref(1))]) |------object(main,main,[]) - Trace: |------’Time: 0, Object: main, Task: 0:main’ |------’Time: 1, Object: GlobalVariables_1, Task: 1:initialize’ |------’Time: 2, Object: 0:main(54), Task: 0:main(54)’ |------’Time: 3, Object: Impmain_2, Task: 3:main’ |------’Time: 4, Object: 0:main(56), Task: 0:main(56)’ 72CAP´ ITULO 7. SYCO: SYSTEMATIC TESTING TOOL FOR CONCURRENT OBJECTS |------’Time: 5, Object: Impf_3, Task: 5:f’ |------’Time: 6, Object: Impf_4, Task: 6:f’ |------’Time: 7, Object: GlobalVariables_1, Task: 9:setvar’ |------’Time: 8, Object: GlobalVariables_1, Task: 7:setvar’ |------’Time: 9, Object: Impf_3, Task: 5:f(34)’ |------’Time: 10, Object: Impf_4, Task: 6:f(34)’ donde podemos ver las dos trazas obtenidas. Para un ejemplo m´as elaborado como es 1int var; 2int var2; 3 4int main () { 5thread f(); 6thread g(); 7return 0; 8} 9 10 void f() { 11 var = 1; 12 var = 2; 13 } 14 15 void g() { 16 var2 = 10 * var + var; 17 } cuya traducci´on “resumida” es 1module Cabs; 2import * from ABS . StdLib ; 3 4interface GLOBAL { 5Int getvar (); 6Unit setvar (Int val ); 7Int getvar2 (); 8Unit setvar2 (Int val ); 9Unit initialize (); 10 } 11 class GlobalVariables () implements GLOBAL { 12 Int var = 0; 13 Int var2 = 0; 14 Unit initialize () { 15 } 16 Int getvar () { 17 return var; 73 18 } 19 Unit setvar (Int val ) { 20 var = val ; 21 } 22 Int getvar2 () { 23 return var2; 24 } 25 Unit setvar2 (Int val ) { 26 var2 = val ; 27 } 28 } 29 30 interface Intf { 31 Unit f(); 32 } 33 34 interface Intg { 35 Unit g(); 36 } 37 38 interface Intmain { 39 Int main (); 40 } 41 42 class Impf ( GLOBAL globalval ) implements Intf { 43 Unit f() { 44 Int aux_var_0 = 1; 45 await globalval ! setvar( aux_var_0 ); 46 Int aux_var_1 = 2; 47 await globalval ! setvar( aux_var_1 ); 48 } 49 } 50 51 class Impg ( GLOBAL globalval ) implements Intg { 52 Unit g() { 53 Int aux_var_2 = 10; 54 Int aux_var_3 = await globalval ! getvar () ; 55 Int aux_var_4 = ( aux_var_2 * aux_var_3 ); 56 Int aux_var_5 = await globalval ! getvar () ; 57 Int aux_var_6 = ( aux_var_4 + aux_var_5 ); 58 await globalval ! setvar2 ( aux_var_6 ); 59 } 60 } 61 62 class Impmain ( GLOBAL globalval ) implements Intmain { 63 Int main () {