Síntesis de código de bajo nivel mediante programación con restricciones

SÍNTESIS DE CÓDIGO DE BAJO NIVEL MEDIANTE PROGRAMACIÓN CON RESTRICCIONES LOW-LEVEL CODE SYNTHESIS USING CONSTRAINT PROGRAMMING TRABAJO FIN DE GRADO CURSO 2023-2024 AUTORES BEATRIZ AEDO DÍAZ CLAUDIA LÓPEZ-MINGO MORENO DIRECTORES ALBERT RUBIO GIMENO ALEJANDRO HERNÁNDEZ CEREZO GRADO EN INGENIERÍA INFORMÁTICA FACULTAD DE INFORMÁTICA UNIVERSIDAD COMPLUTENSE DE MADRID SÍNTESIS DE CÓDIGO DE BAJO NIVEL MEDIANTE PROGRAMACIÓN CON RESTRICCIONES LOW-LEVEL CODE SYNTHESIS USING CONSTRAINT PROGRAMMING TRABAJO DE FIN DE GRADO EN INGENIERÍA INFORMÁTICA AUTORES BEATRIZ AEDO DÍAZ CLAUDIA LÓPEZ-MINGO MORENO DIRECTORES ALEJANDRO HERNÁNDEZ CEREZO ALBERT RUBIO GIMENO CONVOCATORIA: JUNIO 2024 GRADO EN INGENIERÍA INFORMÁTICA FACULTAD DE INFORMÁTICA UNIVERSIDAD COMPLUTENSE DE MADRID 27 DE MAYO DE 2024 RESUMEN Síntesis de Código de Bajo Nivel Mediante Programación con Restricciones La super-optimización es una técnica que busca encontrar la secuencia de instrucciones óptima a una dada explorando secuencias equivalentes. Esta técnica es muy efectiva resolviendo optimizaciones complejas, pero implementarla es muy costosa computacionalmente. En este trabajo de fin de grado buscamos explorar técnicas escalables que han sido propuestas en herramientas para super-optimizar lenguajes de máquinas de pila. Estas técnicas pueden manejar diferentes criterios de optimización y pueden ser adaptadas para diferentes tipos de lenguajes basados en pila. Se ha desarrollado un modelo en MiniZinc para super-optimizar a dos lenguajes de estos: la Ethereum Virtual Machine (EVM) y WebAssembly (Wasm). Para ambos lenguajes se examinan diferentes objetivos de optimización que son relevantes en sus respectivos contextos. Además, se proponen diferentes mecanismos para mejorar la escalabilidad de este enfoque y evaluar su impacto en la propuesta inicial. Se ha evaluado nuestro modelo en un conjunto significativo de ejemplos y se ha podido demostrar que este modelo puede manejar, de forma efectiva, bloques de código de tamaño significativo y optimizarlos, hasta bloques de instrucciones que ya han sido optimizados. Palabras clave EVM, Wasm, super-optimización, MiniZinc, optimización, restricción. ABSTRACT Low-level Code Synthesis Using Constraint Programming Super-optimization is a technique that seeks to find the optimal instruction sequence for a given one by exploring equivalent sequences. This technique is very effective in solving complex optimizations but implementing it is very demanding computationally speaking. This project seeks to explore scalable techniques that have been proposed to super-optimize stack-based bytecode languages. These techniques can manage different optimization criteria and can be modified for different types of stack-based bytecode languages. A model in MiniZinc has been developed to super-optimize two different stack-based bytecode languages: the Ethereum Virtual Machine (EVM) and WebAssembly (Wasm). For both languages different optimization criteria that are relevant in their respective contexts are examined. Furthermore, different mechanisms are proposed to improve the scalability of this approach and evaluate their impact on the initial proposal. The model has been evaluated over significant benchmark sets, and it has been possible to demonstrate that this model can effectively handle and optimize blocks of code of a significant size, even those which have been previously optimized. Keywords EVM, Wasm, super-optimization, MiniZinc, optimization, constraint. ÍNDICE DE CONTENIDOS Capítulo 1 - Introducción...........................................................................................................1 1.1 Motivación........................................................................................................................1 1.2 Objetivos...........................................................................................................................2 1.3 Plan de trabajo................................................................................................................ 3 Capítulo 2 - Introduction............................................................................................................5 2.1 Motivation.........................................................................................................................5 2.2 Goals................................................................................................................................. 6 2.3 Work plan..........................................................................................................................7 Capítulo 3 - Estado de la Cuestión...........................................................................................9 3.1 Lenguajes de Pila.............................................................................................................9 3.1.1 Ethereum Virtual Machine..................................................................................... 9 3.1.2 WebAssembly........................................................................................................11 3.2 Super-optimización........................................................................................................12 3.3 La Programación con Restricciones y MiniZinc..........................................................14 3.3.1 Especificación en MiniZinc.................................................................................. 15 3.3.2 Resolutor.................................................................................................................17 Capítulo 4 - Modelado del Problema....................................................................................18 4.1 Datos de Entrada...........................................................................................................18 4.2 Solución...........................................................................................................................20 4.3 Variables y Constantes................................................................................................. 22 4.4 Pila Inicial y Final.............................................................................................................25 4.5 Dependencias de Memoria.........................................................................................25 4.6 Operaciones de Pila......................................................................................................26 4.6.1 Operación Nop.....................................................................................................26 4.6.2 Operación Pop..................................................................................................... 27 4.6.3 Operaciones DupX...............................................................................................28 4.6.4 Operaciones SwapX.............................................................................................29 4.6.5 Operaciones Zeroarias.........................................................................................30 4.6.6 Operaciones Unarias............................................................................................31 4.6.7 Operaciones Binarias........................................................................................... 32 configura una pila con variables simbólicas que representan su contenido inicial y lo ejecuta simbólicamente. Por último, Superstack [1] codifica el problema como un problema de satisfacción booleana (SAT) para producir eficientemente la secuencia super-optimizada. Un ejemplo de cómo puede ser super-optimizada una secuencia de instrucciones es el siguiente. La secuencia de instrucciones “SWAP1 ADD SWAP1 SUB” super-optimizada da el siguiente resultado: “ADD SWAP1 SUB”. Como se puede observar, el modelo utiliza la propiedad conmutativa del ADD para conseguir el mismo resultado con menos instrucciones, ahorrando la ejecución de un SWAP1 que no es necesario, minimizando así su coste y tamaño. En este trabajo de fin de grado se busca explorar técnicas escalables que han sido propuestas en la herramienta de Superstack [1] pero reemplazando la generación de la codificación SAT por un modelo de MiniZinc, debido a que es una herramienta bastante eficiente que hace muy sencillo el prototipado de nuevas funcionalidades. 1.2 Objetivos Los objetivos de este TFG son los siguientes: 1. Modelar el problema de generar automáticamente fragmentos óptimos de código de bajo nivel para Ethereum Virtual Machine (EVM), basándose en lo ya modelado por Superstack [1], utilizando la herramienta de programación con restricciones MiniZinc. Se implementa a partir de restricciones un modelo del problema y se optimiza usando nuevas restricciones para reducir el espacio de soluciones y, por tanto, acortar la búsqueda. 2. Modelar ese mismo problema para WebAssembly, teniendo en cuenta que este lenguaje, al contrario que EVM, incluye la gestión de registros y puede realizar 2 operaciones sobre ellos. Además, los objetivos de optimización son diferentes, ya que ya no es interesante reducir gas, que es un concepto relacionado con los smart-contracts, o el tamaño en bytes, sino el número de operaciones. 3. Modelar nuevas extensiones para el modelo de EVM a. Implementación de una restricción con el objetivo de reducir aún más la búsqueda en la optimización. b. Soporte de la asociatividad en operaciones binarias. c. La liberalización de la pila de salida. Esto se realiza relajando las condiciones de super-optimización para buscar secuencias válidas y no necesariamente equivalentes a las de partida, ya que se permite cambiar el orden de los elementos de la pila de salida. 1.3 Plan de trabajo Enero 2024 ●Programación utilizando MiniZinc de ejemplos sencillos, obtenidos de la ejecución simbólica de Superstack [1], sin entrada de datos ni operaciones de memoria. Febrero 2024 ●Implementación de la entrada de datos a las soluciones existentes. ●Creación de un modelo generalizado para EVM que sirviese para todos los ejemplos programados anteriormente. Marzo 2024 ●Redacción de los capítulos “Modelado del Problema” y “Estado de la Cuestión” de la memoria y edición de esta. ●Introducción de las operaciones de memoria en el modelo EVM. 3 ●Programación de scripts en Bash que sirvieran para la ejecución simultánea de múltiples ejemplos. Abril 2024 ●Redacción de los capítulos “Introducción”, “Estado de la Cuestión” y “Contribuciones Personales” de la memoria y edición de esta. ●Introducción de restricciones sobre el tamaño y el consumo en el modelo EVM. ●Extensión del modelo para WebAssembly: editando el script “dzn_generation.py” que genera los archivos de datos de MiniZinc, editando el modelo de MiniZinc para las operaciones de Wasm e introduciendo las operaciones SETx, TEEx y GETx. ●Modelado de las operaciones asociativas y conmutativas en el modelo EVM y modificación del script “dzn_generation.py” para adaptarse a las nuevas necesidades de datos de entrada y llevar a cabo el aplanamiento de instrucciones. Mayo 2024 ●Redacción de los capítulos restantes de la memoria y edición de esta. ●Experimentación con el modelo creado para WebAssembly. ●Introducción de la liberalización de pila en el modelo EVM y otras restricciones adicionales. Experimentación con estas extensiones. 4 Capítulo 2 - Introduction 2.1 Motivation In the last decade, blockchain technology has been used increasingly, from finance to supply chains. Ethereum is a blockchain platform that has extended the capacities of cryptocurrency by allowing the execution of smart contracts [10]. These smart contracts are executed in the Ethereum Virtual Machine (EVM), a decentralized execution environment, in exchange for a monetary payment paid in gas, a clear example of criteria that compilers of smart contracts should optimize. Gas is a computational unit used to measure how much it costs to execute an online transaction. Another criterion which would be interesting to optimize is the size in bytes of instructions. The maximum size of smart contracts in Ethereum is 24 kB and also, when the contract is installed you must pay for the bytes it occupies, so bigger smart contracts may need to reduce this value [5]. Another byte-based stack code solution is WebAssembly, which is a language mainly used in high performance web applications [9]. We have seeked to optimize the number of instructions in each sequence because it would better its efficiency and performance and, also, it would minimize the size of the code. Super-optimization is a technique which seeks to find the optimal sequence of instructions by exploring equivalent sequences. This technique is very effective in solving complex optimization problems, but it is very costly to implement computationally speaking. The tool Superstack [1] allows to optimize bytecode of different stack machine architectures, including EVM and Webassembly. This tool extracts the different code sequences that are going to be super-optimized, configures a stack with symbolic variables that represent its initial content and executes it symbolically. Lastly, Superstack 5 [1] codifies the problem like a Boolean satisfaction problem (SAT) to efficiently produce the super-optimized sequence. An example of how a sequence of instructions may be super-optimized is the following. The sequence of instructions “SWAP1 ADD SWAP1 SUB” when super-optimized gives the following result: “ADD SWAP1 SUB”. It can be observed that the model uses the instruction ADD’s commutative property to get the same result with less instructions, saving the execution of a SWAP1 instruction which is not necessary, minimizing the cost and size. This project seeks to explore scalable techniques that have been proposed by Superstack [1] but replacing the generation of SAT codification for a MiniZinc model, due to it being a very efficient tool that makes the prototyping of new functionalities very easy. 2.2 Goals The main goals of this project are: 1. To model the problem of automatically generating optimized fragments of low-level code for Ethereum Virtual Machine (EVM), based on what has already been modeled by Superstack [1], utilizing the constraint programming tool MiniZinc. Based on certain constraints a model of the problem has been programmed and optimized using new constraints to narrow the solution space, shortening the search. 2. To model the same problem for WebAssembly, taking into account that this language, unlike EVM, includes the management of registers and can perform operations on them. Also, the optimization objectives are different, as it is not 6 interesting to minimize gas and bytes, which are concepts relative to smart-contracts, but the number of operations in each sequence. 3. Model new extensions for the EVM code: ○The implementation of a new constraint that seeks further reducing searches during optimization. ○Associativity in binary operations support. ○Output stack liberalization. This last extension is done by relaxing super-optimization conditions so MiniZinc can seek sequences that are valid but not equivalent to the initial ones, as the order of the output stack elements can be changed. 2.3 Work plan January 2024 ●Programming with MiniZinc of simple examples, obtained from the symbolic execution of Superstack [1], without data input or memory operations. February 2024 ●Implementation of data inputs for the existing solutions. ●Creation of a generalized EVM model that would serve for all of the examples programmed earlier. March 2024 ●Drafting of chapters “Modelado del Problema” and “Estado de la Cuestión” of this report and editing of the report. ●Introduction of memory operations in the EVM model. ●Programming of Bash scripts that would serve for the simultaneous execution of multiple examples. 7 April 2024 ●Drafting of chapters “Introducción”, “Estado de la Cuestión” and “Contribuciones Personales” of this report and editing of the report. ●Introduction of constraints upon the size and cost in the EVM model. ●Extension of the model for WebAssembly: editing the “dzn_generation.py” script that generates the MiniZinc data files, adapting the MiniZinc model for Wasm operations and introducing the operations SETx, TEEx and GETx. ●Modeling of associative and commutative operations for EVM mode and modification of the “dzn_generation.py” script to adapt it to new input requirements and associativity. May 2024 ●Drafting of remaining chapters of this report and editing of the report. ●Experimentation with the WebAssembly model. ●Introduction of Stack liberalization and other new constraints in EVM model. Experimentation with these extensions. 8 Capítulo 3 - Estado de la Cuestión 3.1 Lenguajes de Pila 3.1.1 Ethereum Virtual Machine La Ethereum Virtual Machine o EVM es una máquina virtual basada en pila que se especifica en el “Yellow Paper” de Ethereum [10]. Ethereum aumenta las capacidades de las tecnologías blockchain permitiendo ejecutar contratos inteligentes. El “Yellow Paper” [10] establece el consumo de gas para cada instrucción ejecutada, el gas se paga en una unidad fraccionaria de la criptomoneda. El gas es el coste económico que tiene cada operación que se ejecuta en una transacción de un smart contract. El coste total de una transacción suele oscilar entre céntimos y el coste de ejecución. Por esta razón, es útil reducir la cantidad de gas que se invierte en una secuencia de instrucciones. Además del gas, también es interesante reducir el tamaño en bytes (size) de las instrucciones por el deployment, la instalación del smart-contract en la blockchain. Todas las operaciones de pila ocupan 1 byte excepto las operaciones Push, cuyo tamaño depende del valor a apilar. Sabiendo esto, puede ser conveniente para valores muy grandes (hasta 32 bytes) sustituir operaciones Push por otras que resulten en el mismo estado de la pila. Según [7] la EVM almacena datos en tres regiones: almacenamiento, memoria y la pila. El almacenamiento es una región que tiene cada cuenta de Ethereum en la cual se mapea, de forma clave-valor, palabras de 256 bits a otras palabras de 256 bits. No es posible listar el almacenamiento desde un smart contract y es bastante costoso 9 realizar operaciones de lectura y modificación en él. Un contrato no puede acceder al almacenamiento que no sea el de su cuenta. La memoria es linear y puede ser accedida a nivel de byte, los smart contracts obtienen una instancia limpia de ella en cada llamada. Pero las operaciones de escritura cuestan más cuanto mayor sea la palabra y la memoria cuesta más cuanto más grande sea. La pila tiene un tamaño máximo de 1024 elementos y todas las operaciones son ejecutadas sobre ella, además, el acceso a esta está limitado a los 16 elementos en la cima [7]. Las instrucciones desapilan los argumentos necesarios (puede ser que la instrucción no requiera argumentos) para la entrada de cada instrucción específica y apilan el resultado si es que producen un valor de salida. En EVM contamos con 4 operaciones básicas de manipulación de la pila: ●NOP: Es la operación vacía, no realiza ningún cambio a la pila. ●POP: La operación Pop desapila la cima de la pila y descarta el valor desapilado. ●DUPX: Dup es la operación de duplicado. Aparece acompañada de un número entero x que indica el elemento de la pila a duplicar. Si se numeran las posiciones de la pila asignándole el 1 a la cima, el 2 a la subcima y así sucesivamente, dup selecciona el valor en la posición x y lo apila en la cima. La EVM tiene un total de 16 operaciones DUP (de DUP1 a DUP16). ●SWAPX: Swap es la operación de intercambio. Aparece acompañada de un número entero x que indica el elemento de la pila a intercambiar. En este tipo de operación se numeran las posiciones de la pila asignándole el 1 a la subcima, el 2 al elemento inferior a la subcima y así sucesivamente. Swap selecciona el valor en la posición x y lo intercambia por aquel que se encuentra en la cima. Es decir, después de Swap, la posición x contendrá la antigua cima 10 y la cima contendrá el anterior valor que estaba en la posición x de la pila. La EVM tiene un total de 16 operaciones SWAP (de SWAP1 a SWAP16). Existen una gran cantidad de otras operaciones, pero en este trabajo se consideran todas ellas como funciones no interpretadas. Las que sí vamos a describir son algunas de las operaciones de memoria y almacenamiento que realiza EVM. ●MLOAD: cargar una palabra en la pila de la memoria. ●MSTORE: cargar una palabra en la memoria de la pila. ●SLOAD: cargar una palabra de almacenamiento en la pila. ●SSTORE: cargar una palabra de la pila en el almacenamiento. 3.1.2 WebAssembly Tomando como referencia el artículo de “WebAssembly Specification“ [9], WebAssembly o Wasm es una solución para código de bajo nivel en la web desarrollada por un grupo comunitario de W3C, que proporciona una semántica segura, rápida y portable junto con una representación segura y eficiente. Este lenguaje es usado principalmente en aplicaciones web de alto rendimiento, aunque su especificación no contiene características específicas para la Web. Wasm es un lenguaje de código de bytes basado en pilas. En este lenguaje, el código consiste en secuencias de instrucciones que son ejecutadas en orden. Según “WebAssembly Specification” [9] las instrucciones en Wasm operan sobre una pila de operandos, consumiendo argumentos y produciendo o devolviendo resultados. Además de los argumentos dinámicos de la pila, algunas instrucciones también tienen argumentos inmediatos estáticos, normalmente índices o anotaciones de tipo, que forman parte de la instrucción. Algunas instrucciones están estructuradas 11 Capítulo 4 - Modelado del Problema. El problema que se ha planteado para este TFG es la creación de un programa en Minizinc que determine en base a una entrada de datos (que será descrita más adelante) el orden en el que deben ejecutarse ciertas secuencias de operaciones de bajo nivel con el objetivo de optimizarlas. Optimizaremos el código en base al número de operaciones, gas, y tamaño en bytes de las operaciones. Para la generación de soluciones se han añadido los siguientes parámetros a la llamada del programa. ●Opción “--output-time” que imprime el tiempo que tarda en encontrar una solución. ●Opción “-i” que añade a la impresión de la solución las soluciones intermedias que MiniZinc haya encontrado. 4.1 Datos de Entrada Los datos de entrada provienen de la fase de ejecución simbólica de la herramienta SuperStack [1] y son proporcionados en formato JSON. Para que MiniZinc pueda procesarlos hay que transformarlos a ficheros de datos de MiniZinc o DZN. Esto se ha hecho mediante el script de “dzn_generation.py”, el cual es explicado con más detalle en el quinto capítulo. Como ha sido mencionado anteriormente, los datos que se proporcionan al programa de MiniZinc mediante el DZN son introducidos como constantes en el programa. El DZN proporciona todas las constantes necesarias para que el modelo pueda calcular la forma más eficiente de resolver el problema. No se van a mencionar todas las constantes definidas, pero sí algunas de las más relevantes. 18 ●Enumerado TERM: contiene todos los valores que pueden tomar los elementos de la pila. Se incluye un valor especial, el valor nulo, para representar la posibilidad de que un elemento de la pila no contenga ningún valor. ●Array de dependencias: contiene todas las dependencias de memoria. Las operaciones de memoria, es decir, las operaciones Load y Store, funcionan de forma diferente que el resto ya que pueden influir en otras operaciones de memoria. En particular, varios accesos a la misma posición de memoria pueden devolver resultados diferentes si esta se modifica. La forma de solucionarlo es con una abstracción de en qué orden pueden aparecer las operaciones. Se marcan parejas de operaciones de memoria como dependientes una de la otra, que es lo que se codifica en el modelo y se explica posteriormente. ●Tamaño máximo de la pila y número máximo de operaciones. Son constantes esenciales para la inicialización y recorrido de vectores y enumerados. ●Enumerados con los tipos de operaciones SwapX y DupX que pueden ser realizadas. Se introduce una operación de cada tipo para cada X entre el 1 y el máximo especificado en EVM. El funcionamiento de estas operaciones se explicará más adelante. ●Arrays con los contenidos de la pila en el primer y último estado denominados “starstack” y “endstack”, respectivamente. Hay cinco tipos de operaciones que pueden aparecer en el DZN, si una operación está definida en él entonces tendrá que ser ejecutada obligatoriamente, es decir, aparecerá en el resultado. Estas operaciones pueden ser Zeroarias, Unarias, Binarias, Push o Store. La lógica de cada una será explicada posteriormente. Para cada tipo de operación, el DZN incluirá una serie de parámetros. ●Número de operaciones de ese tipo. Sirve sobre todo para poder declarar los vectores asociados correctamente. 19 ●Enumerados que representan cada cómputo del tipo correspondiente. Cada uno contiene la lista de los nombres de los cómputos de ese tipo, a los cuales se identifica inequívocamente. ●Arrays que contienen los términos de entrada y salida de ese tipo, siendo los términos de entrada los elementos que ese tipo de operación consume (desapilándolos) y los términos de salida los que genera (y añade a la cima de la pila) ese tipo de operación. La operación necesitará que los términos de entrada se encuentren en la cima para poder ejecutarse. El número de arrays dependerá de las necesidades de ese tipo de operación. Por ejemplo, las operaciones Zeroarias (que no consumen ningún elemento y producen un elemento) sólo tienen un array llamado “zeroout”; pero las operaciones Unarias (que consumen un elemento y producen otro, tienen dos arrays) uno que contiene los términos de entrada llamado “unin” y otro los de salida llamado “unout”. ●Array con el valor de gas para cada una de las operaciones de ese tipo. ●Array con el valor de size para cada una de las operaciones de ese tipo. ●En caso de las operaciones Binarias, también tendrán un array de booleanos que indiquen si esa operación es conmutativa o no. 4.2 Solución En la Figura 4-2 se muestra un ejemplo de lo que contiene la solución de un problema concreto. Se puede observar cómo aparecen las soluciones posibles por orden decreciente de coste en función de la función objetivo especificada, siendo la última aquella que consigue la mayor optimización. Cada solución posible muestra lo siguiente: 20 ●Según el criterio de optimización: el número de instrucciones, el gas utilizado o el size utilizado. ●El array “fgas” que contiene el gas de cada operación asignada en ese estado. ●El array “fsize” que contiene el tamaño de cada operación asignada en ese estado. ●El array “program” que contiene las operaciones a ejecutar de un estado a otro, en el orden en el que se deben ejecutar. El array debe estar definido con un tamaño y tipo constantes, lo que nos obliga a declararlo con el tamaño equivalente a la cantidad máxima de instrucciones. Esto conlleva que a menudo el array no se llene entero, sin embargo, debemos darles un valor a todas las posiciones. Por ello usamos Nop como representación de ninguna operación. ●La matriz “states” de estados de la pila, siendo la primera fila el estado inicial y las siguientes filas el estado de la pila después de aplicar la operación asignada en el estado anterior. Es decir, la segunda fila mostrará el estado de la pila una vez la primera operación ha sido ejecutada, y así sucesivamente hasta llegar al estado final de pila, que resulta de todas las instrucciones ejecutadas. De manera similar a Nop en el array “program”, esta matriz incluye también espacios vacíos o valores “null”, ya que la matriz se construye con un tamaño fijo equivalente al número máximo de estados por el número máximo de elementos en la pila. Así, cada vez que en un estado la pila no está llena, podemos ver el valor ‘.’, que también forma parte del enumerado TERM definido anteriormente. De esta manera, podemos definir “states” como una matriz de tipo TERM para usar una representación acorde con MiniZinc. ●“Time elapsed” se refiere al tiempo que ha tardado MiniZinc en encontrar dicha solución. 21 Figura 4.2. Ejemplo de solución 4.3 Variables y Constantes Aparte de los datos introducidos por el DZN también han sido necesarias la declaración de ciertas constantes, principalmente para almacenar valores intermedios que posteriormente serán utilizados por alguna restricción. Se han creado diferentes instancias de “set of int” que representan distintos rangos de acceso para nuestros arrays y enumerados. Estos conjuntos han sido muy útiles a la hora de recorrer las estructuras de la implementación, ya que aportan el rango de números entre los dos valores deseados. Algunos de estos conjuntos son los siguientes: ●SS: conjunto que representa el rango [1, tamaño del programa]. ●SN: conjunto que representa el rango [1, tamaño de la pila]. ●MDN: conjunto que representa el rango [1, número de dependencias de memoria]. Las variables son los elementos que forman la solución, definidos en el comienzo de este capítulo. Además, entre las variables también se encuentran los elementos utilizados para la optimización, explicada posteriormente. 22 OPCODES es un tipo enumerado que se ha creado para facilitar el manejo de los códigos de operación. En la ejecución del programa existen un número diferente de operaciones distintas según el código a procesar, por este motivo es necesaria una manera de nombrarlas dentro del propio código. Además, es importante de cara a la declaración del array “program”. Este enumerado está compuesto por todos los enumerados de los diferentes tipos de operaciones (“DUP_ENUM”, “SWAP_ENUM”, “ZEROARYOP”, “UNARYOP”, “BINARYOP”, “PUSHOP”, “STOROP”) junto con las operaciones Nop y Pop. Esto se ha podido realizar gracias a que MiniZinc permite extender los enumerados a través de sus constructores, de tal forma que se puede convertir un elemento de un enumerado a otro usando la función del constructor, llamada F, o su inversa, llamada F^-1. El Enum OPCODES se declara de la manera usual en MiniZinc. Es inicializado igualándolo a la unión de los diferentes Enums que existen en la implementación y, además, se añaden las operaciones Nop y Pop. Para sumar estos Enums se usa un constructor diferente para cada Enum, que los transforma a tipo Opcodes. Cada una de estas funciones tiene un nombre distinto. Ahora, Opcodes contiene una enumeración de todos los códigos de operación que se pueden utilizar para nuestra solución. Figura 4.3-1. Enumerado Opcodes Cuando se utiliza la función F sobre el Enum original, se revisa el contenido de ese Enum interpretándose como parte de Opcodes. Es decir, la función devuelve un valor de tipo Opcodes en vez del tipo del Enum original. Cuando se utiliza la función inversa F^-1 sobre un valor de tipo Opcodes, devuelve el índice de ese valor en el Enum original del cual proviene. De esta manera, 23 la función inversa permite usar el índice sobre los arrays del tipo de instrucción deseado. Un ejemplo sería el siguiente: en la definición anterior de OPCODES, SW(SWAP_ENUM) se utiliza para representar los términos del enumerado SWAP_ENUM como parte de OPCODES. Este mismo constructor se aplica a los términos del enumerado inicial para crear el término correspondiente en el enumerado extendido. Por ejemplo, SWAP2 corresponde al valor en el enumerado SWAP_ENUM, y SW(SWAP2) se corresponde con el valor correspondiente en el enumerado de OPCODES. Con Opcodes listo para su uso se puede utilizar como tipo para el array program, que contendrá la solución final. Sin Opcodes, la implementación cambiaría drásticamente, ya que permite usar todas las operaciones como un solo tipo y a la vez diferenciar los subtipos dentro del enumerado, pudiendo distinguir las restricciones adecuadas a cada operación concreta. Figura 4.3-2. Array Program El enumerado Opcodes es utilizado en la mayoría de las restricciones de diversas formas. 1. Identificar el tipo de instrucción que se va a manejar. Al comienzo de cada restricción se comprueba comparando directamente con una posición del de OPCODES (e.g. Nop, Pop) o comprobando si la instrucción forma parte de uno de los Enums que forman OPCODES (por ejemplo, “DUP_ENUM”, “SWAP_ENUM”, etc.) Figura 4.3-3. Identificación de tipo de instrucción - Por posición 24 Figura 4.3-4. Identificación de tipo de instrucción - Por enum 2. Obtener la posición que ocupa la operación en su Enum original. Para poder acceder a los datos de las operaciones (parámetros de entrada y salida, gas, size, etc.), se necesita conocer su posición en el Enum original, ya que el valor que se encuentra en el array program hace referencia a su posición en Opcodes. Para ello, utilizamos la función inversa. Figura 4.3-5. Obtención de la posición de una instrucción 4.4 Pila Inicial y Final Para garantizar la equivalencia entre la secuencia encontrada y la original, la primera restricción definida obliga a que el primer estado de la pila sea igual a “startstack” y el último estado de la pila sea igual a “endstack”. Se implementa de una manera iterativa, asegurando que cada uno de los elementos del primer y del último estado son iguales a cada uno de los elementos de los datos que se tienen sobre la entrada y la salida. Figura 4.4. Restricción de primer y último estado de la pila 4.5 Dependencias de Memoria Se implementan las dependencias de memoria ya mencionadas para asegurar que los datos obtenidos en los accesos a memoria son los correctos y no han sido sobrescritos en un orden inadecuado. Esta información se proporciona en el archivo DZN en forma de un vector de duplas de instrucciones en el que cada dupla 25 representa una dependencia. Su significado es que una vez se ejecuta la segunda operación de la dupla, no se debe ejecutar la primera. Lo que quiere decir que, al tener la obligación de ejecutar todas las operaciones proporcionadas, la primera operación de la dupla debe ejecutarse obligatoriamente antes que la segunda. Figura 4.5. Restricción dependencias memoria 4.6 Operaciones de Pila En esta sección, se definirán las restricciones que modelan el impacto de las operaciones sobre la pila. Adicionalmente, se detallarán las restricciones que se han creado para satisfacer la ejecución de dichas operaciones. 4.6.1 Operación Nop Nop es la “no operación”, es decir, cuando este término aparece en la solución es que en ese estado no se ejecuta ninguna operación. Esta operación es necesaria ya que nuestro modelo fija un tamaño máximo de operaciones inicial y así se pueden encontrar soluciones en las que se ejecuten menos operaciones. Como se detalla anteriormente, el array solución debe asignar una instrucción a cada posición y usamos Nop como “relleno”. La restricción codificada para modelar esta operación obliga a que se cumplan dos condiciones cuando es aplicada en un determinado estado. 1. Las operaciones en los estados que restan deben ser también Nop. Así evitamos diferentes versiones de una misma solución que solo difieran en la posición de Nops. 2. En el siguiente estado, la pila se debe mantener igual. 26 Asimismo, en la codificación de la restricción se incorpora una condición que añada los valores correspondientes de gas y size a los arrays de “fgas” y “fsize”. La operación Nop tiene valores nulos para los criterios de gas y size. Figura 4.6.1. Restricción Nop 4.6.2 Operación Pop Pop es una operación que desapila el primer elemento de la pila y lo descarta. Esta operación obliga a que se cumplan dos condiciones cuando es aplicada. 1. En el estado sobre el cual se ejecuta, la primera posición de la pila no puede ser igual al valor nulo, ya que la pila debe contener al menos un elemento. 2. En el siguiente estado, al consumir el primer elemento, todos los elementos de la pila a partir del segundo se desplazan hacia la izquierda. Además, el último elemento será igual al valor nulo por la necesidad de asignar un valor a cada posición de la matriz. Asimismo, en la restricción se incluye una condición que añada los valores correspondientes de gas y size a los arrays de “fgas” y “fsize”. La operación Pop tiene valores fijos para gas y size de 2 y 1, respectivamente. Figura 4.6.2. Restricción Pop 27 Figura 4.6.7. Restricción Binaria 4.6.8 Operaciones Push La operación Push inserta un elemento en la primera posición de la pila. Se puede considerar un caso especial de operación Zeroaria. Las consideramos en una categoría diferente porque son las únicas instrucciones cuyo tamaño en bytes no es 1, sino que depende del valor que se introduzca. Superstack [1] define restricciones adicionales específicas para estas operaciones, por lo que hemos decidido mantenerlas en una categoría independiente. Esta operación se comporta como las operaciones Zeroarias. Figura 4.6.8. Restricción Push 4.6.9 Operaciones Store Store es la operación de inserción en memoria, que requiere los dos elementos en la primera y segunda posición de la pila, pudiendo considerarla un caso especial de operación Binaria sin elemento de salida. En la codificación de la restricción, primero, se identifica dentro de su Enumerado asociado la posición de la operación 34 Store que está siendo analizada (x). Esta operación obliga a que se cumplan ciertas condiciones cuando es aplicada en un determinado estado. 1. En ese estado, el elemento en la primera posición de la pila debe ser igual al elemento en la posición x en el array de “storin1” y el elemento en la segunda posición de la pila debe ser igual al elemento en la posición x en el array de “storin2”. Este tipo de operación no dispone de la opción de conmutatividad ya que cada uno de los elementos consumidos se usará de manera diferente. 2. En el siguiente estado, los elementos en la última y penúltima posición de la pila deben ser nulos, ya que dos elementos han sido consumidos. 3. En el siguiente estado, al haber consumido dos elementos, todos los elementos en la pila a partir del tercero se desplazan dos posiciones a la izquierda para evitar la aparición de valores nulos o incorrectos en la cima y subcima. La restricción sobre el gas y el tamaño se aplica de la misma manera que en las operaciones Zeroarias pero utilizando sus arrays correspondientes. Figura 4.6.9. Restricción Store 4.7 Restricciones Adicionales Finalmente, se han añadido ciertas restricciones para la optimización y para facilitar al resolutor la búsqueda de soluciones. 35 4.7.1 Optimización La optimización tiene un rol importante en la programación con restricciones, ya que es la forma de que MiniZinc encuentre la solución más óptima en función de una función objetivo específica. En el caso de este proyecto hemos incluido tres criterios de optimización, codificados de la forma que muestra la Figura 4.7.1-1. 1. El resolutor minimiza el número de instrucciones en el programa. Como el tamaño del array “program” es constante, este criterio es equivalente a maximizar el número de Nops. Esta codificación es mucho más sencilla y directa, por lo que se ha adaptado esta representación en nuestro modelo. 2. El resolutor minimiza el gas total utilizado, es decir, la suma del gas que utiliza cada una de las operaciones que forman parte de nuestra solución. 3. El resolutor minimiza el size total utilizado, es decir, la suma de size correspondiente a cada una de las operaciones que forman parte de nuestra solución. Se elige un modo de optimización mediante dos variables, “option” toma valores entre el 0 y el 2 determinando cuál de las tres opciones vamos a usar. Por otro lado, ”value” toma su valor dependiendo de “option”. Este puede ser el número de operaciones, la suma de gas o la suma de size. Una vez elegido el valor para “value”, minimizamos su valor. En particular, para el número de instrucciones minimizamos el número máximo de operaciones menos el número de Nops. Figura 4.7.1-1. Restricción Zeros, gas y size 36 Figura 4.7.1-2. Minimización de value 4.7.2 Forzar la Aparición de Operaciones Esta restricción obliga a que cada operación en los enums de “ZEROARYOP”, “UNARYOP”, “BINARYOP”, “STOROP” y “PUSHOP” aparezcan en el programa. Esta restricción ayuda a recortar el espacio de soluciones y ejecutar más rápido ya que elimina todas las soluciones en las cuales no aparezcan las operaciones que tienen que ser ejecutadas. Esta restricción es obligatoria en el caso de operaciones Store, ya que en el caso contrario una solución puede prescindir de aplicarlas, al no generar ningún elemento de pila. Figura 4.7.2. Restricción operaciones 4.7.3 Cada Elemento Usado Debe Ser Insertado Para recortar el espacio de búsqueda, esta restricción obliga a que cada elemento presente en cualquiera de los arrays de los datos de entrada (“unin”, “binin1”, “binin2”, “storin1”, “storin2”) o en la pila de salida (“endstack”), debe aparecer en la pila de entrada (“startstack”) o en los arrays de los datos de salida (“zeroout”, “unout”, “binout”, “pushout”). Esta condición se cumple sin necesidad de especificar la restricción, sin embargo, acorta el tiempo de ejecución ya que no considera las soluciones que serían descartadas más tarde por incorrectas. La implementación pasa por comprobar uno a uno que cada elemento de los arrays de entrada y pila inicial está presente por lo menos en uno de los arrays de salida o pila final. 37 Figura 4.7.3. Restricción de elementos usados e insertados. 4.7.4 No Introducir Elementos Antes de una Instrucción Pop Para recortar el espacio de búsqueda de cara a la optimización, esta restricción obliga a no apilar elementos justo antes de descartarlos con una instrucción pop. Si lleváramos a cabo tal acción, tendríamos en cuenta soluciones poco óptimas en las que el resultado de una operación carecería de utilidad. Descartando dichas soluciones a través de esta restricción aceleramos la búsqueda de secuencias más prometedoras. La implementación de esta restricción consiste en comprobar que, si la instrucción actual es Pop, la anterior debe ser necesariamente Pop o Swap. Figura 4.7.4. Restricción inserción antes de Pop. 4.7.5 Limitar las operaciones con coste de gas mayor o igual que 3 Esta restricción busca generar menos resultados poco óptimos. Para no obtener costes en gas demasiado altos, las operaciones que tengan un coste en gas mayor o igual que tres pueden ejecutarse una sola vez. La implementación de la restricción recorre uno a uno el Enum de cada tipo de instrucción. Para cada instrucción comprueba si su valor de gas es igual o mayor que tres. Si es así, asegura que esta instrucción aparezca en la solución como máximo una 38 vez. Esto resultará siempre en una aparición si tenemos en cuenta la restricción que definimos en el apartado 4.7.2. Figura 4.7.5. Restricción alto coste en gas 39 Capítulo 5 - Experimentación En esta sección, evaluamos los mecanismos propuestos en el capítulo 4 y en los Apéndices A y B sobre un conjunto significativo de ejemplos, que corresponden a un subconjunto de los programas utilizados en la evaluación experimental del artículo de SuperStack [1]: ●Una colección de 10 programas escritos en Circom de la biblioteca Circom, un DSL para crear circuitos aritméticos en pruebas de conocimiento-cero. ●Una compilación de 10 contratos de código optimizados que también se emplearon en la evaluación de la herramienta de super-optimización GASOL, precursora de SuperStack [1]. Los experimentos se han realizado en una máquina AMD Ryzen Threadripper PRO 3995WX, con 64 cores y 512 GB de memoria, que ejecuta Debian 5.10.7. Los resultados mostrados en este capítulo demuestran que el modelo MiniZinc codificado en este proyecto encuentra soluciones equivalentes para secuencias complejas en un tiempo razonable. Estas secuencias habían sido optimizadas previamente por sus respectivos compiladores, lo que demuestra aún más el impacto de la técnica de super-optimización. Las pruebas que se han realizado han sido sobre las extensiones de este proyecto, explicadas en los dos apéndices. Se ha ejecutado el modelo de MiniZinc creado para EVM y Wasm para cada uno de los ficheros de datos de ejemplo. Utilizando el comando “--time-limit” de MiniZinc, se restringió el tiempo que podía tardar el modelo en encontrar una solución para cada ejemplo. Cuando el modelo tardaba más de lo establecido, la ejecución se detenía, mostrando un mensaje similar al siguiente: 40 Figura 5. Ejemplo de Timeout. Aunque se pare la ejecución del modelo antes de que haya encontrado la solución óptima, MiniZinc imprime también las soluciones intermedias que ha encontrado. Esto es útil para analizar cuánto tiempo se tarda en encontrar cada solución mejorada. Los datos se han obtenido ejecutando scripts reutilizados de Superstack [1] que se nos han proporcionado para procesar los ficheros de resultados de los ejemplos. Estos scripts miden entre otras cosas el consumo en gas y size (en el caso de EVM) y el número de instrucciones (en el caso de Wasm) para determinar las ganancias correspondientes según el criterio seleccionado, además de otra información como, por ejemplo, el tiempo de ejecución y si se ha conseguido probar la optimalidad de la última secuencia encontrada. También se ha reutilizado un checker de Superstack [1] que ha comprobado que todas las soluciones encontradas son equivalentes a las de partida. En particular, se ha extendido el checker para comprobar las condiciones de asociatividad-conmutatividad y también para la liberalización de las restricciones de la pila final (estas extensiones se explican en el apéndice B). Todo el código que se ha utilizado en este TFG se puede encontrar en este repositorio de GitHub: https://github.com/beaaedo/tfg.fdi.ucm.Aedo.Lopez-Mingo 5.1 Scripts adicionales Los siguientes scripts han sido creados para ejecutar y procesar el modelo de MiniZinc con los diferentes programas analizados. 41 5.1.1 Conversión de formato JSON a DZN Como se ha indicado previamente, las secuencias a analizar se han proporcionado en formato JSON. Para que MiniZinc fuese capaz de procesar estos archivos tuvieron que ser convertidos a un fichero de datos de MiniZinc o DZN. Para este proyecto han sido creados dos scripts de Python, ambos con el mismo nombre “dzn_generation.py”, pero en diferentes directorios. Uno de los scripts procesa secuencias del lenguaje EVM y el otro de WebAssembly. En forma son relativamente similares, exceptuando que tienen algunos parámetros diferentes ya que ambos lenguajes necesitan diferentes consideraciones y tienen tipos de operaciones diferentes. En este script, se recorren todos los campos del JSON proporcionado y se imprimen las variables correspondientes. Por ejemplo, como se puede ver en la figura 5.1.1, para generar la pila final o "endstack", se crea un array vacío y se recorre el array de la pila final obtenido del JSON, añadiendo los términos al array vacío. A continuación, si la pila tiene menos elementos que su tamaño máximo, se añaden elementos nulos para rellenarla. Por último, se imprime el array al fichero de datos de Minizinc en el formato "endstack = [ Contenido del array endstack ]". Figura 5.1.1. Generación de la pila final en “dzn_generation.py”. 5.1.2 Scripts de Bash Con el fin de simplificar y acortar el proceso de pruebas, ya que existían un número muy amplio de ejemplos que ejecutar; se han creado tres scripts que 42 conviertan los ejemplos de JSON a DZN utilizando el script “dzn_generation.py” correspondiente y, posteriormente, ejecuten el modelo en MiniZinc utilizando el fichero de datos. ●El script “generar_dzn.sh” invoca al script “dzn_generation.py” con todos los archivos de ejemplos en formato JSON, uno a uno, y los almacena en un directorio llamado “ejemplos_dzn”. ●El script “ejecutar_ejemplos.sh” invoca al script de MiniZinc con todos los archivos de ejemplos en formato DZN, uno a uno, y almacena el resultado de la ejecución en un archivo de texto con el contenido de la solución, que posteriormente guarda en un directorio llamado “ejemplos_results”. Separar cada resultado en un fichero de datos puede ser útil en el futuro para analizar los tiempos de todas las secuencias intermedias. Como la ejecución de cada ejemplo es independiente, se ha podido paralelizar la ejecución de las instancias utilizando el comando “parallel”. El comando GNU “parallel” permite ejecutar varios comandos de forma paralela, especificando la cantidad de comandos con el parámetro “-j número_de_comandos”. El uso de mecanismos de paralelización ha permitido acelerar la evaluación experimental. Figura 5.1.2. Uso de GNU Parallel. ●Finalmente, el script “creardzn_ejecutarejemplos.sh” ejecuta los dos scripts definidos anteriormente. Esta estructura de scripts permite desacoplar el proceso de generación de ficheros de datos de MiniZinc de la ejecución de estos, lo cual ha facilitado la 43 Figura 5.2.1-3. Datos de mejora de ahorro en operaciones, gas y size con restricción adicional. El ahorro de operaciones ejecutadas es uno de los aspectos que “Mejorada” no es capaz de mejorar, mientras que las otras configuraciones sí lo hacen. Para ahorrar gas, a pesar de lo anterior y teniendo mejoras con todas las configuraciones, “Mejorada” es la mejor opción. Este resultado se vuelve a repetir cuando se cuantifica el ahorro en size. Con los resultados obtenidos podemos asegurar que la mejor combinación global es “Mejorada”, ya que supera a “Cima_pila” individualmente y a “Todo” en la mayoría de los casos. 5.2.2 Nuevas Extensiones - Aplanamiento Otra de las extensiones que se ha realizado sobre el modelo de EVM es la introducción de la propiedad asociativa como forma de encontrar soluciones, la cual será explicada en el Apéndice B. Una vez conocida la mejor combinación de 50 restricciones hasta ahora (“Mejorada”), se aplica el aplanamiento o asociatividad activando estas restricciones para observar las mejoras que aparecen. Figura 5.2.2-1. Datos de mejora de soluciones encontradas por asociatividad. Se puede ver claramente que la asociatividad no presenta mejoras a la hora de encontrar soluciones, independientemente del estilo de minimización elegido. 51 Figura 5.2.2-2. Datos de mejora en tiempo de ejecución por asociatividad. El tiempo de ejecución se ve reducido siempre que no se minimice size, pero la diferencia es realmente pequeña. Figura 5.2.2-3. Datos de mejora de ahorro en operaciones, gas y size por asociatividad. En el caso del ahorro, ya sea en número de operaciones, gas o size, se ven resultados muy similares para ambas configuraciones. Se observa que estas diferencias tan pequeñas (o incluso nulas) se deben a que el contenido del dataset no explota lo suficiente la asociatividad. De 7483 bloques que se usan como ejemplo, tan solo se aplanan 133, que es una cantidad relativamente pequeña. Se usará un nuevo conjunto de datos para comprobar el impacto real de la asociatividad o aplanamiento. Para ello, construimos 5000 secuencias aleatorias que aplican asociatividad o aplanamiento. Estas secuencias se han generado siguiendo el siguiente procedimiento: 52 ●Se generan secuencias aleatorias de “OPCODES” de un conjunto específico (ADD, MUL, PUSH 1, SUB, MSTORE, MLOAD, SWAP1, SWAP2, SWAP3, DUP1, DUP2, DUP3. A ADD y MUL). A las operaciones conmutativas del conjunto se les asocia el triple de probabilidad de aparecer en las secuencias para que así se tienda a reutilizar cómputos conmutativos alternando otras operaciones. ●Se seleccionan las secuencias que contienen al menos un aplanamiento y cinco como máximo hasta conseguir 5000 ejemplos. En las gráficas se pueden ver los datos procedentes del nuevo dataset donde “AC_Gas” representa los cambios que efectúa la asociatividad cuando se minimiza gas y “AC_Size” cuando se minimiza size. “No_AC_Gas” y “No_AC_Size” representan la ejecución del mismo dataset sin usar asociatividad. Figura 5.2.2-4. Datos de mejora en porcentaje de soluciones encontradas por asociatividad - Nuevo Dataset. Por desgracia, la asociatividad parece empeorar el porcentaje de soluciones encontradas aproximadamente en un 3.5% para minimizaciones de gas y size. 53 Figura 5.2.2-5. Datos de mejora en tiempo de ejecución (s) por asociatividad - Nuevo Dataset. Sin embargo, el tiempo de ejecución sí se reduce y de manera más importante que con el antiguo conjunto de datos. La reducción es de una magnitud parecida entre un criterio de minimización y otro. 54 Figura 5.2.2-6. Datos de mejora en ahorro en gas y size encontradas por asociatividad - Nuevo Dataset. El ahorro tanto en gas como en size se vuelve evidente para este conjunto de datos. Este conjunto de secuencias demuestra que esta extensión mejora el modelo en tiempo de ejecución y ahorro de gas y size, siempre y cuando se aplique aplanamiento de forma extensiva. 5.2.3 Nuevas Extensiones - Liberalización de pila La última extensión que se ha introducido sobre el modelo de EVM es la liberalización de la pila final. Es decir, el estado de pila final debe contener el mismo conjunto de elementos que la pila final dada por el problema, pero no necesariamente en el mismo orden. La liberalización de la pila será explicada en el Apéndice B. Para evaluar esta extensión se han generado restricciones aleatorias de pila sobre la colección de partida. Se han filtrado los bloques que tenían 3 o más elementos en la pila final, ya que es el mínimo que hace falta para que cobre sentido la liberalización. Sobre este grupo filtrado, se ha generado un número aleatorio de restricciones de orden de la pila final (como máximo el número de elementos de esta - 2). Las restricciones se generan seleccionando dos elementos aleatorios de la pila final, forzando a que se mantenga la diferencia de posiciones existente entre ellos. Así se ha asegurado la factibilidad del problema, ya que por construcción la secuencia original cumple las restricciones. El nuevo conjunto de datos consta de 3087 secuencias de instrucciones. En las siguientes gráficas se muestran cuatro ejecuciones distintas. “Mejorada” es la ejecución obtenida de los experimentos anteriores usando las restricciones “Pop” 55 y “Cima_pila”. “Normal” representa una combinación de las mismas restricciones sobre el nuevo conjunto de datos. “Config” indica los datos obtenidos al añadir la liberalización de pila y “Config_AC” incluye además aplanamiento. Figura 5.2.3-1. Datos de mejora en porcentaje de soluciones encontradas por liberalización de pila. La liberalización añade soluciones encontradas cuando se minimiza Gas, quedando el valor para minimización de size ligeramente por debajo que el de “Normal”. Como veíamos en el apartado anterior, la inclusión de asociatividad no favorece a la búsqueda de soluciones. 56 Figura 5.2.3-2. Datos de mejora en tiempo de ejecución (s) por liberalización de pila. Se obtienen unos datos satisfactorios para la reducción del tiempo de ejecución, tanto la liberalización como la liberalización con asociatividad lo reducen de manera visible para cualquier criterio de minimización. 57 Figura 5.2.3-3. Datos de mejora en ahorro en gas y size encontradas por asociatividad. Para terminar, no se ven cambios significativos para el ahorro de gas y size, aunque para la minimización de size se ven pequeños incrementos de ahorro con liberalización de pila, tanto con asociatividad como sin ella. Se concluye que la liberalización de la pila es útil principalmente para reducir el tiempo de ejecución de los ejemplos, pero su combinación con asociatividad no produce mejoras extras. 5.3 Wasm El dataset utilizado para WebAssembly contiene 2256 ejemplos con secuencias de instrucciones de tamaño entre 1 y 20. Hemos optimizado estos ejemplos usando diferentes timeouts. Dado que en Wasm no había que evaluar diferentes extensiones ni diferentes criterios de optimización (como en EVM), se ha decidido evaluar cómo afectan diferentes timeouts a las soluciones encontradas. Se ha ejecutado el modelo 58 de MiniZinc para Wasm utilizando tres límites de tiempo diferentes: 180 segundos, 300 segundos y 420 segundos. El ratio de número de soluciones encontradas y tiempo límite utilizado es el esperado. Cuanto más tiempo se permite ejecutar cada ejemplo, más soluciones encuentra, como se puede ver en la siguiente figura. También es necesario puntualizar que los ejemplos en los cuales no se ha encontrado solución, independientemente del tiempo límite, contienen todos 20 instrucciones a optimizar. Es decir, para ejemplos con un código de 16 instrucciones o menos a optimizar, encuentra una solución optimizada a todos. Figura 5.3-1. Gráfico de Número de Ejemplos vs. Número de Soluciones Encontradas. En cambio, cuanto más alto sea el tiempo límite mayor es la media geométrica de operaciones optimizadas, siendo estas el número de operaciones que contiene cada solución optimizada. Esto se puede explicar fácilmente recordando que, los únicos ejemplos a los cuales no ha encontrado solución son los que contienen 20 59 debido a restricciones de tiempo, el modelo que incorpora esta gestión de simetrías no ha encontrado resultados durante la experimentación para un conjunto significativo de ejemplos, aproximadamente para el 40% de los ejemplos totales. El objetivo de implementar una restricción nueva que redujera más aún la búsqueda se ha cumplido. Los experimentos han demostrado que la restricción relativa a las instrucciones que se pueden haber ejecutado para llegar a una pila con cima X, junto con la relativa a las instrucciones que se pueden ejecutar antes de una operación Pop, es la que ha dado lugar a una mayor optimización. Por desgracia, la combinación de estas restricciones no consigue mejorar el ahorro de operaciones ejecutadas. El soporte de la asociatividad en operaciones binarias se ha implementado exitosamente. Sin embargo, no consigue el objetivo de aumentar el número de soluciones encontradas. Esto hace que se plantee la posibilidad de limitar la cantidad de ejemplos en el conjunto de datos en los que se puede aplicar asociatividad para encontrar más soluciones mientras se optimizan tiempo de ejecución, número de operaciones, gas y size. La liberalización de la pila de salida también se ha implementado de manera correcta dando unos resultados especialmente buenos a la hora de reducir el tiempo de ejecución. Sería interesante visitar la idea de liberalizar la pila de entrada de una manera parecida a la que se ha realizado. 66 Capítulo 7 - Conclusions and future work As it has been defined in the introduction of this document, the objectives of this project were to model with MiniZinc the problem of automatically generating optimized fragments of low-level code for EVM, based on what had already been modeled by Superstack [1], modeling this same problem for Wasm and, finally, the implementation of new extensions for the EVM model, including a constraint with the objective of reducing even more the search in optimization, implementation of associativity and stack liberalization. The first objective, to model the super-optimizer proposed by Superstack [1] in Minizinc, has been successfully achieved. We have been able to successfully model all the constraints proposed by Superstack [1] and “Super optimization of Smart Contracts” [2] and a solution was found for the examples with which the model was tested. In this process, a constraint was implemented (section 4.7.4), modeled before by [2], that provided a good improvement in finding solutions, execution time, operation saving, gas saving and size saving with any of the three minimization types. In regard to the model developed to optimize blocks of code written in the language WebAssembly, even though good results have been obtained during the experimentation phase, it would be beneficial to continue exploring different execution time limits. This would allow us to confirm that the model can find solutions for the lengthiest blocks of code. Also, a strategy that has not been successfully proved is the implementation of symmetry control constraints. This technique searches to avoid the execution of redundant operations with registers, restricting the frequency and moment of occurrence of SetX and TeeX operations. However, due to time restrictions, the model 67 that incorporates this has not found solutions during experimentation for a greater number of examples, approximately 40% of the total number of examples. The goal of implementing a new constraint that could reduce the search even more has been achieved. Experiments demonstrated that the constraint concerning operations that can be executed to get to a stack with x at the top, as well as the one concerning operations that can be executed before a POP operation, is the one that led to a bigger optimization, especially in certain conditions. Sadly, the combination of these two constraints do not add up to operation saving. Associativity support in binary operations has been implemented successfully. Nevertheless, it does not achieve the objective of increasing the number of found solutions. This can be a reason to consider the possibility of reducing the quantity of examples in the dataset in which associativity can be applied so more solutions can be found while execution time, operation number, gas and size are optimized. Final stack liberalization has also been implemented correctly leading to especially good results when reducing execution time. It could be interesting to visit the idea of liberalizing the initial stack in a similar way to what has been done. 68 CONTRIBUCIONES PERSONALES Apéndice A - Aportaciones de Beatriz Aedo Diaz. WebAssembly. Uno de los retos propuestos ha sido la implementación de un modelo de MiniZinc para la optimización de secuencias de código en WebAssembly. Esto ha supuesto cambios significativos en el modelo. La mayor diferencia entre el modelo de EVM y Wasm es la introducción de registros. Este comportamiento se ha modelado añadiendo una matriz con los estados de cada registro. Figura A-1. Solución Wasm. Cambios en Constantes y Variables Con la introducción de la manipulación de registros hay constantes que se han eliminado y otras que se han añadido. Las que se han eliminado son las siguientes. 69 ●Todas las constantes para los tipos de operación Zeroarias, Unarias, Binarias, Push y Store han sido eliminadas ya que, en este modelo, la clasificación en función de la aridad de las operaciones ha sido eliminada para Wasm. Wasm no tiene cinco tipos de operaciones definidas, sino que tiene operaciones que pueden consumir de 0-3 variables de entradas y pueden producir de 0-3 variables de salidas. Por lo que, al ser tan variable, no tiene sentido tener las operaciones definidas por número de entradas y salidas. ●Los enumeradores de las operaciones DupX y SwapX ya que no son operaciones que existan en este lenguaje. Además, las constantes que se han añadido para la gestión de registros son las siguientes. ●El entero 'NR' contiene el número de registros a los cuales se van a aplicar cambios. ●El “max_registers_sz” contiene el número máximo de registros adicionales que pueden ser utilizados. Estos registros adicionales son útiles para poder guardar cómputos intermedios y así reutilizarlos, pudiendo resultar en una mayor optimización. ●El array “register_changes” contiene el estado inicial y final que deben tener los registros. Los valores que están almacenados dentro de los registros pertenecen al enumerado TERM. Se ha definido una nueva variable, añadida en la solución, llamada “register_states”. Esta variable almacena el contenido de los registros en cada estado del programa. 70 Al no haber definido las operaciones en Wasm por tipos, todas las constantes definidas para las operaciones son comunes para todas ellas. Son las siguientes: ●El enumerado “OP” representa cada cómputo. ●El entero “N” es igual al número de cómputos. ●Dos enteros “in_ops” y “out_ops” con el número de parámetros de entrada que consume y el número de parámetros de salida que produce cada operación, respectivamente. ●Arrays con los parámetros de entrada que consume (llamados “in1”, “in2” e “in3”) y el número de parámetros de salida (llamados “out1”, “out2” e “out3”) que produce cada operación. No todas las operaciones consumen y producen tres parámetros por lo que el array contendrá los términos correspondientes que consume y produce y asignará elementos nulos para indicar que no produce ni consume ningún elemento. ●Array “comm” formado por booleanos que indican si la operación correspondiente es conmutativa. Otro cambio importante es que el concepto de gas no existe en Wasm ya que es una métrica de la EVM. El concepto de size si existe en Wasm pero no es de interés estudiarlo. Por tanto, se ha querido estudiar la super-optimización del número de instrucciones. Por lo que, aunque los arrays de gas y size siguen definidos en el modelo para preservar el modelo anterior, han sido igualados a uno en todos los casos. También se han añadido tres tipos de operaciones de manipulación de registros nuevas en Wasm, que no existían para EVM, ya que este es el mecanismo utilizado en este lenguaje para gestionar la pila. Las operaciones son SetX, GetX y TeeX, cuyo funcionamiento será explicado más adelante. De forma similar a DupX y SwapX en EVM, se introducen como constantes tres enumerados con los SetX, GetX y TeeX que se 71 pueden realizar. Las restricciones creadas en el modelo de EVM para la gestión de las operaciones DupX y SwapX también han sido eliminadas. Al haber cambiado la forma en la que se definen las operaciones, el enumerado OPCODES también ha cambiado. Ahora OPCODES está compuesto por todos los enumerados de “SET_ENUM”, “GET_ENUM”, “TEE_ENUM” y “OP” junto con las operaciones Nop y Pop. Figura A-2. Enumerado OPCODES en Wasm. Finalmente, se han definido dos sets of int nuevos. Un conjunto llamado RN que represente el rango [1, NR + max_registers_sz], es decir, que represente todas las posiciones de los registros. Y otro llamado NR1 que represente el rango [1, NR + 1], es decir, que represente las posiciones de los registros que tienen que sufrir modificaciones. Operaciones con Registros A continuación, se van a explicar más en detalle el funcionamiento de las tres operaciones de manipulación de registros nuevas en Wasm. ●SetX: esta operación consume el primer elemento de la pila y lo introduce en el registro X. Se introduce una operación SetX por cada registro disponible. Figura A-3. Operación SetX 72 ●GetX: esta operación introduce en la cima de la pila el valor que esté almacenado en el registro X. Se introduce una operación GetX por cada registro disponible. Figura A-4. Operación GetX ●TeeX: esta operación, en la que X se refiere al número de registros en los que puede realizarse, introduce el primer elemento de la pila en el registro X sin consumirlo. Figura A-5. Operación TeeX Adicionalmente, se han añadido restricciones para la gestión de los registros, que son bastante similares a las restricciones de gestión de la pila. ●En el estado inicial y final de los registros se corresponde con el definido en el array de “register_states”. ●Los registros adicionales inicialmente no deben contener nada, es decir, contienen el valor nulo. Figura A-6. Restricciones de gestión de registros Las operaciones de Nop y Pop se han mantenido iguales, salvo que se ha añadido una condición en ambas para que los registros en el siguiente estado se mantengan igual que en el estado en el que se aplica la operación. 73 Figura A-7. Operaciones Nop y Pop en Wasm. Por último, se ha añadido una restricción que mantiene el mismo valor en los registros después de operaciones que pertenezcan al enumerado OP, ya que esas operaciones no realizan modificaciones en los registros. Figura A-8. Restricciones de operaciones no de registros Operaciones sobre la Pila Como se ha comentado anteriormente, otro de los cambios respecto a EVM es que la clasificación en función de la aridad de las operaciones ha sido eliminada para Wasm. Esto también ha cambiado radicalmente la forma de definir las restricciones de las operaciones en MiniZinc. Ahora hay definidas cuatro restricciones para la gestión de operaciones. Si una operación es conmutativa entonces funcionará igual que una operación Binaria conmutativa en EVM, consumiendo dos elementos y generando uno. Figura A-9. Restricción Wasm para los parámetros de entrada. Conmutativas. 74 Si una operación no es conmutativa entonces consumirá el número de parámetros de entrada que tenga que estén en la cima de la pila en ese estado. Figura A-10. Restricción Wasm para los parámetros de entrada. No conmutativas. Todas las operaciones, dependiendo de la cantidad de parámetros de salida, introducirán los parámetros de salida que tengan en la cima de la pila en el estado siguiente. Figura A-11. Restricción Wasm para los parámetros de salida. Todas las operaciones, además, obligan que se cumplan ciertas condiciones referentes al estado de los elementos de la pila que no han sido modificados por la operación. La restricción se impone dependiendo de la diferencia entre el número de parámetros de salida y de entrada. ●Si el número de parámetros de salida es mayor que el de entrada. 1. En el siguiente estado, los elementos desde el que está en la posición que sigue al número de parámetros de salida hasta el último son iguales al elemento que esté en esa posición menos la resta del número de parámetros de salida menos los de entrada. 2. Los elementos en ese estado en las posiciones últimas, correspondientes con la diferencia entre los parámetros de salida y entrada, deben ser nulos. 75 Figura B-4. Restricción ASSOCIATIVEADDOP. Liberalización de la Pila Final En la versión original de la codificación para EVM las pilas de entrada y salida son fijas. Es decir, para satisfacer el problema se debe llegar a una solución cuyo primer estado de pila sea exactamente igual que la pila de entrada y el último estado exactamente igual que la pila de salida. En esta extensión, se relaja esta condición fundamental para el proceso de super-optimización para así explorar secuencias que no son exactamente equivalentes a las de partida, pero que realizan los mismos cómputos. Se introduce el concepto de la liberalización de la pila final. Esto quiere decir que el estado de pila final debe contener el mismo conjunto de elementos que la pila final dada por el problema, pero no necesariamente en el mismo orden. Esta extensión trata de mejorar el código en el contexto del programa del que ha sido extraído, explorando distintos órdenes en los elementos de la pila cuando se alcanzan los bloques sucesores del CFG. Para asegurar que la pila final sigue siendo válida para su uso en el siguiente bloque se imponen unas condiciones que limitan la liberalización. Las restricciones que se imponen sobre la pila de salida representan la posición relativa de un elemento respecto a otro. Concretamente se indica la distancia que hay entre ambos de la siguiente manera. Recibimos una tupla con esta forma: (S_i, S_j, k) 82 Que nos da la siguiente información: Pos(S_i) + k <= Pos(S_j) Donde Pos(x) es la posición del elemento de tipo “TERM” en la pila final. Para la implementación en MiniZinc seguimos varios pasos: ●Modificamos el script “dzn_generation.py”. Se añade la opción de que el archivo JSON a leer contenga un campo “order_tgt_ws”. Si el JSON no contiene dicho campo significa que la ejecución será como hasta ahora, si está presente pero es vacío se incorporará liberalización de pila sin dependencias y si encontramos un campo “order_tgt_ws” con contenido se tendrán en cuenta las dependencias para la liberalización. El script además escribirá sobre el DZN las nuevas constantes necesarias declaradas en MiniZinc. ●Se incluyen nuevas constantes a la codificación de MiniZinc: el Booleano “lib” indica si se aplicará liberalización o no, el entero “nlib” representa el número de dependencias (0 si lib = false), el array “lib_elem” contiene una pareja de elementos por dependencia que muestran los elementos sobre los que aplicar la dependencia (S_i y S_j) y por último el array “lib_dis” contiene el valor “k” que concreta la distancia entre elementos. Figura B-5. Constantes para liberalización. ●Se modifica la restricción relativa a la pila de entrada para usarla únicamente en caso de no aplicar liberalización. Ahora la ejecución de la restricción está condicionada por la constante “lib”. 83 Figura B-6. Cambio de restricción pila de salida. ●Se agrega una nueva restricción para la pila final que cubre el caso “lib” = true. Esta restricción consiste en comprobar que cada elemento existente aparece el mismo número de veces en la pila final dada por el problema y la pila final del resultado. Con esto se indica que la pila final generada está compuesta del mismo conjunto de elementos que la pila final que se recibió como dato de entrada. Figura B-7. Restricción de pila de salida con liberalización. ●Se codifica una restricción adicional que implementa las posiciones relativas entre elementos de la pila final. Para ello, se definen dos variables a y b que representan las posiciones de S_i y S_j. Se buscan valores que pueden tomar a y b de tal manera que la posición a de la pila final sea S_i (lib_elem[i,1]) y la posición b sea S_j (lib_elem[i,2]). Los valores encontrados para a y b se usan en la condición ya explicada: {a + lib_dis[i] <= b donde lib_dis[i] representa el valor k}. Esta comprobación se repite para todas las condiciones que existan respecto a las posiciones de la pila final (un total de nlib). Figura B-8. Restricción liberalización con condiciones. 84 BIBLIOGRAFÍA [1] Albert, E., Garcia de la Banda, M., Hernández-Cerezo, A., Ignatiev, A., Rubio, A., & Stuckley, P. J. (2024, Junio). SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. ACM Program,Lang. 8, PLDI(Artículo 205), 26 páginas. https://doi.org/10.1145/3656435 [2] Albert, E., Gordillo, P., Hernández-Cerezo, A., Rubio, A., & Schett, M. A. (2022, Julio). Super optimization of Smart Contracts. ACM Trans,Softw. Eng. Methodol. 31, 4, 70, 29 páginas. https://doi.org/10.1145/3506800 [3] Apt, K. (2003). Principles of constraint programming. Cambridge University Press. https://books.google.es/books?id=1e7Ib04fZAcC&lpg=PR11&dq=%20Principles%2 0of%20Constraint%20Programming&lr&hl=es&pg=PR2#v=onepage&q=isbn&f=fal se [4] Chu, G., Stuckey, P. J., Schutt, A., Ehlers, T., Gange, G., & Francis, K. (2015). Chuffed, a lazy clause generation solver. GitHub. Retrieved May 20, 2024, from https://github.com/chuffed/chuffed?tab=readme-ov-file [5] Holst Swende, M., Bylica, P., Beregszaszi, A., & Maiboroda, A. (2021, Julio). EIP-3860: Limit and meter initcode. Ethereum Improvement Proposals, (no. 3860). https://eips.ethereum.org/EIPS/eip-3860 85 [6] Saraswat, V., & Van Hentenryck, P. (1995). Principles and Practice of Constraint Programming: The Newport Papers (V. Saraswat & P. Van Hentenryck, Eds.; Vol. MiniZinc: Towards a Standard CP Modelling Language). NetLibrary, Incorporated. [7] The Solidity Authors & ethereum.org. (2016). Introduction to Smart Contracts — Solidity 0.8.27 documentation. Solidity Documentation. Retrieved May 24, 2024, from https://docs.soliditylang.org/en/latest/introduction-to-smart-contracts.html [8] Stuckey, P. J., Marriott, K., & Tac, G. (2020). Specification of MiniZinc. Minizinc. Retrieved May 20, 2024, from https://www.minizinc.org/doc-2.8.4/en/spec.html [9] WebAssembly Community Group & Rossberg, A. (2024, 4 28). WebAssembly Specification. Retrieved May 20, 2024, from https://webassembly.github.io/gc/core/_download/WebAssembly.pdf [10] Wood, G. (2014). Ethereum: A secure decentralised generalised transaction ledger. https://ethereum.github.io/yellowpaper/paper.pdf. https://ethereum.github.io/yellowpaper/paper.pdf 86