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ín esis de Código de Bajo Ni el Median e P og amación con Res icciones La supe -op imización es una écnica que busca encon a la secuencia de ins ucciones óp ima a una dada explo ando secuencias equi alen es. Es a écnica es muy e ec i a esol iendo op imizaciones complejas, pe o implemen a la es muy cos osa compu acionalmen e. En es e abajo de in de g ado buscamos explo a écnicas escalables que han sido p opues as en he amien as pa a supe -op imiza lenguajes de máquinas de pila. Es as écnicas pueden maneja di e en es c i e ios de op imización y pueden se adap adas pa a di e en es ipos de lenguajes basados en pila. Se ha desa ollado un modelo en MiniZinc pa a supe -op imiza a dos lenguajes de es os: la E he eum Vi ual Machine (EVM) y WebAssembly (Wasm). Pa a ambos lenguajes se examinan di e en es obje i os de op imización que son ele an es en sus espec i os con ex os. Además, se p oponen di e en es mecanismos pa a mejo a la escalabilidad de es e en oque y e alua su impac o en la p opues a inicial. Se ha e aluado nues o modelo en un conjun o signi ica i o de ejemplos y se ha podido demos a que es e modelo puede maneja , de o ma e ec i a, bloques de código de amaño signi ica i o y op imiza los, has a bloques de ins ucciones que ya han sido op imizados. Palab as cla e EVM, Wasm, supe -op imización, MiniZinc, op imización, es icción. ABSTRACT Low-le el Code Syn hesis Using Cons ain P og amming Supe -op imiza ion is a echnique ha seeks o ind he op imal ins uc ion sequence o a gi en one by explo ing equi alen sequences. This echnique is e y e ec i e in sol ing complex op imiza ions bu implemen ing i is e y demanding compu a ionally speaking. This p ojec seeks o explo e scalable echniques ha ha e been p oposed o supe -op imize s ack-based by ecode languages. These echniques can manage di e en op imiza ion c i e ia and can be modi ied o di e en ypes o s ack-based by ecode languages. A model in MiniZinc has been de eloped o supe -op imize wo di e en s ack-based by ecode languages: he E he eum Vi ual Machine (EVM) and WebAssembly (Wasm). Fo bo h languages di e en op imiza ion c i e ia ha a e ele an in hei espec i e con ex s a e examined. Fu he mo e, di e en mechanisms a e p oposed o imp o e he scalabili y o his app oach and e alua e hei impac on he ini ial p oposal. The model has been e alua ed o e signi ican benchma k se s, and i has been possible o demons a e ha his model can e ec i ely handle and op imize blocks o code o a signi ican size, e en hose which ha e been p e iously op imized. Keywo ds EVM, Wasm, supe -op imiza ion, MiniZinc, op imiza ion, cons ain . ÍNDICE DE CONTENIDOS Capí ulo 1 - In oducción...........................................................................................................1 1.1 Mo i ación........................................................................................................................1 1.2 Obje i os...........................................................................................................................2 1.3 Plan de abajo................................................................................................................ 3 Capí ulo 2 - In oduc ion............................................................................................................5 2.1 Mo i a ion.........................................................................................................................5 2.2 Goals................................................................................................................................. 6 2.3 Wo k plan..........................................................................................................................7 Capí ulo 3 - Es ado de la Cues ión...........................................................................................9 3.1 Lenguajes de Pila.............................................................................................................9 3.1.1 E he eum Vi ual Machine..................................................................................... 9 3.1.2 WebAssembly........................................................................................................11 3.2 Supe -op imización........................................................................................................12 3.3 La P og amación con Res icciones y MiniZinc..........................................................14 3.3.1 Especi icación en MiniZinc.................................................................................. 15 3.3.2 Resolu o .................................................................................................................17 Capí ulo 4 - Modelado del P oblema....................................................................................18 4.1 Da os de En ada...........................................................................................................18 4.2 Solución...........................................................................................................................20 4.3 Va iables y Cons an es................................................................................................. 22 4.4 Pila Inicial y Final.............................................................................................................25 4.5 Dependencias de Memo ia.........................................................................................25 4.6 Ope aciones de Pila......................................................................................................26 4.6.1 Ope ación Nop.....................................................................................................26 4.6.2 Ope ación Pop..................................................................................................... 27 4.6.3 Ope aciones DupX...............................................................................................28 4.6.4 Ope aciones SwapX.............................................................................................29 4.6.5 Ope aciones Ze oa ias.........................................................................................30 4.6.6 Ope aciones Una ias............................................................................................31 4.6.7 Ope aciones Bina ias........................................................................................... 32 con igu a una pila con a iables simbólicas que ep esen an su con enido inicial y lo ejecu a simbólicamen e. Po úl imo, Supe s ack [1] codi ica el p oblema como un p oblema de sa is acción booleana (SAT) pa a p oduci e icien emen e la secuencia supe -op imizada. Un ejemplo de cómo puede se supe -op imizada una secuencia de ins ucciones es el siguien e. La secuencia de ins ucciones “SWAP1 ADD SWAP1 SUB” supe -op imizada da el siguien e esul ado: “ADD SWAP1 SUB”. Como se puede obse a , el modelo u iliza la p opiedad conmu a i a del ADD pa a consegui el mismo esul ado con menos ins ucciones, aho ando la ejecución de un SWAP1 que no es necesa io, minimizando así su cos e y amaño. En es e abajo de in de g ado se busca explo a écnicas escalables que han sido p opues as en la he amien a de Supe s ack [1] pe o eemplazando la gene ación de la codi icación SAT po un modelo de MiniZinc, debido a que es una he amien a bas an e e icien e que hace muy sencillo el p o o ipado de nue as uncionalidades. 1.2 Obje i os Los obje i os de es e TFG son los siguien es: 1. Modela el p oblema de gene a au omá icamen e agmen os óp imos de código de bajo ni el pa a E he eum Vi ual Machine (EVM), basándose en lo ya modelado po Supe s ack [1], u ilizando la he amien a de p og amación con es icciones MiniZinc. Se implemen a a pa i de es icciones un modelo del p oblema y se op imiza usando nue as es icciones pa a educi el espacio de soluciones y, po an o, aco a la búsqueda. 2. Modela ese mismo p oblema pa a WebAssembly, eniendo en cuen a que es e lenguaje, al con a io que EVM, incluye la ges ión de egis os y puede ealiza 2 ope aciones sob e ellos. Además, los obje i os de op imización son di e en es, ya que ya no es in e esan e educi gas, que es un concep o elacionado con los sma -con ac s, o el amaño en by es, sino el núme o de ope aciones. 3. Modela nue as ex ensiones pa a el modelo de EVM a. Implemen ación de una es icción con el obje i o de educi aún más la búsqueda en la op imización. b. Sopo e de la asocia i idad en ope aciones bina ias. c. La libe alización de la pila de salida. Es o se ealiza elajando las condiciones de supe -op imización pa a busca secuencias álidas y no necesa iamen e equi alen es a las de pa ida, ya que se pe mi e cambia el o den de los elemen os de la pila de salida. 1.3 Plan de abajo Ene o 2024 ●P og amación u ilizando MiniZinc de ejemplos sencillos, ob enidos de la ejecución simbólica de Supe s ack [1], sin en ada de da os ni ope aciones de memo ia. Feb e o 2024 ●Implemen ación de la en ada de da os a las soluciones exis en es. ●C eación de un modelo gene alizado pa a EVM que si iese pa a odos los ejemplos p og amados an e io men e. Ma zo 2024 ●Redacción de los capí ulos “Modelado del P oblema” y “Es ado de la Cues ión” de la memo ia y edición de es a. ●In oducción de las ope aciones de memo ia en el modelo EVM. 3 ●P og amación de sc ip s en Bash que si ie an pa a la ejecución simul ánea de múl iples ejemplos. Ab il 2024 ●Redacción de los capí ulos “In oducción”, “Es ado de la Cues ión” y “Con ibuciones Pe sonales” de la memo ia y edición de es a. ●In oducción de es icciones sob e el amaño y el consumo en el modelo EVM. ●Ex ensión del modelo pa a WebAssembly: edi ando el sc ip “dzn_gene a ion.py” que gene a los a chi os de da os de MiniZinc, edi ando el modelo de MiniZinc pa a las ope aciones de Wasm e in oduciendo las ope aciones SETx, TEEx y GETx. ●Modelado de las ope aciones asocia i as y conmu a i as en el modelo EVM y modi icación del sc ip “dzn_gene a ion.py” pa a adap a se a las nue as necesidades de da os de en ada y lle a a cabo el aplanamien o de ins ucciones. Mayo 2024 ●Redacción de los capí ulos es an es de la memo ia y edición de es a. ●Expe imen ación con el modelo c eado pa a WebAssembly. ●In oducción de la libe alización de pila en el modelo EVM y o as es icciones adicionales. Expe imen ación con es as ex ensiones. 4 Capí ulo 2 - In oduc ion 2.1 Mo i a ion In he las decade, blockchain echnology has been used inc easingly, om inance o supply chains. E he eum is a blockchain pla o m ha has ex ended he capaci ies o c yp ocu ency by allowing he execu ion o sma con ac s [10]. These sma con ac s a e execu ed in he E he eum Vi ual Machine (EVM), a decen alized execu ion en i onmen , in exchange o a mone a y paymen paid in gas, a clea example o c i e ia ha compile s o sma con ac s should op imize. Gas is a compu a ional uni used o measu e how much i cos s o execu e an online ansac ion. Ano he c i e ion which would be in e es ing o op imize is he size in by es o ins uc ions. The maximum size o sma con ac s in E he eum is 24 kB and also, when he con ac is ins alled you mus pay o he by es i occupies, so bigge sma con ac s may need o educe his alue [5]. Ano he by e-based s ack code solu ion is WebAssembly, which is a language mainly used in high pe o mance web applica ions [9]. We ha e seeked o op imize he numbe o ins uc ions in each sequence because i would be e i s e iciency and pe o mance and, also, i would minimize he size o he code. Supe -op imiza ion is a echnique which seeks o ind he op imal sequence o ins uc ions by explo ing equi alen sequences. This echnique is e y e ec i e in sol ing complex op imiza ion p oblems, bu i is e y cos ly o implemen compu a ionally speaking. The ool Supe s ack [1] allows o op imize by ecode o di e en s ack machine a chi ec u es, including EVM and Webassembly. This ool ex ac s he di e en code sequences ha a e going o be supe -op imized, con igu es a s ack wi h symbolic a iables ha ep esen i s ini ial con en and execu es i symbolically. Las ly, Supe s ack 5 [1] codi ies he p oblem like a Boolean sa is ac ion p oblem (SAT) o e icien ly p oduce he supe -op imized sequence. An example o how a sequence o ins uc ions may be supe -op imized is he ollowing. The sequence o ins uc ions “SWAP1 ADD SWAP1 SUB” when supe -op imized gi es he ollowing esul : “ADD SWAP1 SUB”. I can be obse ed ha he model uses he ins uc ion ADD’s commu a i e p ope y o ge he same esul wi h less ins uc ions, sa ing he execu ion o a SWAP1 ins uc ion which is no necessa y, minimizing he cos and size. This p ojec seeks o explo e scalable echniques ha ha e been p oposed by Supe s ack [1] bu eplacing he gene a ion o SAT codi ica ion o a MiniZinc model, due o i being a e y e icien ool ha makes he p o o yping o new unc ionali ies e y easy. 2.2 Goals The main goals o his p ojec a e: 1. To model he p oblem o au oma ically gene a ing op imized agmen s o low-le el code o E he eum Vi ual Machine (EVM), based on wha has al eady been modeled by Supe s ack [1], u ilizing he cons ain p og amming ool MiniZinc. Based on ce ain cons ain s a model o he p oblem has been p og ammed and op imized using new cons ain s o na ow he solu ion space, sho ening he sea ch. 2. To model he same p oblem o WebAssembly, aking in o accoun ha his language, unlike EVM, includes he managemen o egis e s and can pe o m ope a ions on hem. Also, he op imiza ion objec i es a e di e en , as i is no 6 in e es ing o minimize gas and by es, which a e concep s ela i e o sma -con ac s, bu he numbe o ope a ions in each sequence. 3. Model new ex ensions o he EVM code: ○The implemen a ion o a new cons ain ha seeks u he educing sea ches du ing op imiza ion. ○Associa i i y in bina y ope a ions suppo . ○Ou pu s ack libe aliza ion. This las ex ension is done by elaxing supe -op imiza ion condi ions so MiniZinc can seek sequences ha a e alid bu no equi alen o he ini ial ones, as he o de o he ou pu s ack elemen s can be changed. 2.3 Wo k plan Janua y 2024 ●P og amming wi h MiniZinc o simple examples, ob ained om he symbolic execu ion o Supe s ack [1], wi hou da a inpu o memo y ope a ions. Feb ua y 2024 ●Implemen a ion o da a inpu s o he exis ing solu ions. ●C ea ion o a gene alized EVM model ha would se e o all o he examples p og ammed ea lie . Ma ch 2024 ●D a ing o chap e s “Modelado del P oblema” and “Es ado de la Cues ión” o his epo and edi ing o he epo . ●In oduc ion o memo y ope a ions in he EVM model. ●P og amming o Bash sc ip s ha would se e o he simul aneous execu ion o mul iple examples. 7 Ap il 2024 ●D a ing o chap e s “In oducción”, “Es ado de la Cues ión” and “Con ibuciones Pe sonales” o his epo and edi ing o he epo . ●In oduc ion o cons ain s upon he size and cos in he EVM model. ●Ex ension o he model o WebAssembly: edi ing he “dzn_gene a ion.py” sc ip ha gene a es he MiniZinc da a iles, adap ing he MiniZinc model o Wasm ope a ions and in oducing he ope a ions SETx, TEEx and GETx. ●Modeling o associa i e and commu a i e ope a ions o EVM mode and modi ica ion o he “dzn_gene a ion.py” sc ip o adap i o new inpu equi emen s and associa i i y. May 2024 ●D a ing o emaining chap e s o his epo and edi ing o he epo . ●Expe imen a ion wi h he WebAssembly model. ●In oduc ion o S ack libe aliza ion and o he new cons ain s in EVM model. Expe imen a ion wi h hese ex ensions. 8 Capí ulo 3 - Es ado de la Cues ión 3.1 Lenguajes de Pila 3.1.1 E he eum Vi ual Machine La E he eum Vi ual Machine o EVM es una máquina i ual basada en pila que se especi ica en el “Yellow Pape ” de E he eum [10]. E he eum aumen a las capacidades de las ecnologías blockchain pe mi iendo ejecu a con a os in eligen es. El “Yellow Pape ” [10] es ablece el consumo de gas pa a cada ins ucción ejecu ada, el gas se paga en una unidad acciona ia de la c ip omoneda. El gas es el cos e económico que iene cada ope ación que se ejecu a en una ansacción de un sma con ac . El cos e o al de una ansacción suele oscila en e cén imos y el cos e de ejecución. Po es a azón, es ú il educi la can idad de gas que se in ie e en una secuencia de ins ucciones. Además del gas, ambién es in e esan e educi el amaño en by es (size) de las ins ucciones po el deploymen , la ins alación del sma -con ac en la blockchain. Todas las ope aciones de pila ocupan 1 by e excep o las ope aciones Push, cuyo amaño depende del alo a apila . Sabiendo es o, puede se con enien e pa a alo es muy g andes (has a 32 by es) sus i ui ope aciones Push po o as que esul en en el mismo es ado de la pila. Según [7] la EVM almacena da os en es egiones: almacenamien o, memo ia y la pila. El almacenamien o es una egión que iene cada cuen a de E he eum en la cual se mapea, de o ma cla e- alo , palab as de 256 bi s a o as palab as de 256 bi s. No es posible lis a el almacenamien o desde un sma con ac y es bas an e cos oso 9 ealiza ope aciones de lec u a y modi icación en él. Un con a o no puede accede al almacenamien o que no sea el de su cuen a. La memo ia es linea y puede se accedida a ni el de by e, los sma con ac s ob ienen una ins ancia limpia de ella en cada llamada. Pe o las ope aciones de esc i u a cues an más cuan o mayo sea la palab a y la memo ia cues a más cuan o más g ande sea. La pila iene un amaño máximo de 1024 elemen os y odas las ope aciones son ejecu adas sob e ella, además, el acceso a es a es á limi ado a los 16 elemen os en la cima [7]. Las ins ucciones desapilan los a gumen os necesa ios (puede se que la ins ucción no equie a a gumen os) pa a la en ada de cada ins ucción especí ica y apilan el esul ado si es que p oducen un alo de salida. En EVM con amos con 4 ope aciones básicas de manipulación de la pila: ●NOP: Es la ope ación acía, no ealiza ningún cambio a la pila. ●POP: La ope ación Pop desapila la cima de la pila y desca a el alo desapilado. ●DUPX: Dup es la ope ación de duplicado. Apa ece acompañada de un núme o en e o x que indica el elemen o de la pila a duplica . Si se nume an las posiciones de la pila asignándole el 1 a la cima, el 2 a la subcima y así sucesi amen e, dup selecciona el alo en la posición x y lo apila en la cima. La EVM iene un o al de 16 ope aciones DUP (de DUP1 a DUP16). ●SWAPX: Swap es la ope ación de in e cambio. Apa ece acompañada de un núme o en e o x que indica el elemen o de la pila a in e cambia . En es e ipo de ope ación se nume an las posiciones de la pila asignándole el 1 a la subcima, el 2 al elemen o in e io a la subcima y así sucesi amen e. Swap selecciona el alo en la posición x y lo in e cambia po aquel que se encuen a en la cima. Es deci , después de Swap, la posición x con end á la an igua cima 10 y la cima con end á el an e io alo que es aba en la posición x de la pila. La EVM iene un o al de 16 ope aciones SWAP (de SWAP1 a SWAP16). Exis en una g an can idad de o as ope aciones, pe o en es e abajo se conside an odas ellas como unciones no in e p e adas. Las que sí amos a desc ibi son algunas de las ope aciones de memo ia y almacenamien o que ealiza EVM. ●MLOAD: ca ga una palab a en la pila de la memo ia. ●MSTORE: ca ga una palab a en la memo ia de la pila. ●SLOAD: ca ga una palab a de almacenamien o en la pila. ●SSTORE: ca ga una palab a de la pila en el almacenamien o. 3.1.2 WebAssembly Tomando como e e encia el a ículo de “WebAssembly Speci ica ion“ [9], WebAssembly o Wasm es una solución pa a código de bajo ni el en la web desa ollada po un g upo comuni a io de W3C, que p opo ciona una semán ica segu a, ápida y po able jun o con una ep esen ación segu a y e icien e. Es e lenguaje es usado p incipalmen e en aplicaciones web de al o endimien o, aunque su especi icación no con iene ca ac e ís icas especí icas pa a la Web. Wasm es un lenguaje de código de by es basado en pilas. En es e lenguaje, el código consis e en secuencias de ins ucciones que son ejecu adas en o den. Según “WebAssembly Speci ica ion” [9] las ins ucciones en Wasm ope an sob e una pila de ope andos, consumiendo a gumen os y p oduciendo o de ol iendo esul ados. Además de los a gumen os dinámicos de la pila, algunas ins ucciones ambién ienen a gumen os inmedia os es á icos, no malmen e índices o ano aciones de ipo, que o man pa e de la ins ucción. Algunas ins ucciones es án es uc u adas 11 Capí ulo 4 - Modelado del P oblema. El p oblema que se ha plan eado pa a es e TFG es la c eación de un p og ama en Minizinc que de e mine en base a una en ada de da os (que se á desc i a más adelan e) el o den en el que deben ejecu a se cie as secuencias de ope aciones de bajo ni el con el obje i o de op imiza las. Op imiza emos el código en base al núme o de ope aciones, gas, y amaño en by es de las ope aciones. Pa a la gene ación de soluciones se han añadido los siguien es pa áme os a la llamada del p og ama. ●Opción “--ou pu - ime” que imp ime el iempo que a da en encon a una solución. ●Opción “-i” que añade a la imp esión de la solución las soluciones in e medias que MiniZinc haya encon ado. 4.1 Da os de En ada Los da os de en ada p o ienen de la ase de ejecución simbólica de la he amien a Supe S ack [1] y son p opo cionados en o ma o JSON. Pa a que MiniZinc pueda p ocesa los hay que ans o ma los a iche os de da os de MiniZinc o DZN. Es o se ha hecho median e el sc ip de “dzn_gene a ion.py”, el cual es explicado con más de alle en el quin o capí ulo. Como ha sido mencionado an e io men e, los da os que se p opo cionan al p og ama de MiniZinc median e el DZN son in oducidos como cons an es en el p og ama. El DZN p opo ciona odas las cons an es necesa ias pa a que el modelo pueda calcula la o ma más e icien e de esol e el p oblema. No se an a menciona odas las cons an es de inidas, pe o sí algunas de las más ele an es. 18 ●Enume ado TERM: con iene odos los alo es que pueden oma los elemen os de la pila. Se incluye un alo especial, el alo nulo, pa a ep esen a la posibilidad de que un elemen o de la pila no con enga ningún alo . ●A ay de dependencias: con iene odas las dependencias de memo ia. Las ope aciones de memo ia, es deci , las ope aciones Load y S o e, uncionan de o ma di e en e que el es o ya que pueden in lui en o as ope aciones de memo ia. En pa icula , a ios accesos a la misma posición de memo ia pueden de ol e esul ados di e en es si es a se modi ica. La o ma de soluciona lo es con una abs acción de en qué o den pueden apa ece las ope aciones. Se ma can pa ejas de ope aciones de memo ia como dependien es una de la o a, que es lo que se codi ica en el modelo y se explica pos e io men e. ●Tamaño máximo de la pila y núme o máximo de ope aciones. Son cons an es esenciales pa a la inicialización y eco ido de ec o es y enume ados. ●Enume ados con los ipos de ope aciones SwapX y DupX que pueden se ealizadas. Se in oduce una ope ación de cada ipo pa a cada X en e el 1 y el máximo especi icado en EVM. El uncionamien o de es as ope aciones se explica á más adelan e. ●A ays con los con enidos de la pila en el p ime y úl imo es ado denominados “s a s ack” y “ends ack”, espec i amen e. Hay cinco ipos de ope aciones que pueden apa ece en el DZN, si una ope ación es á de inida en él en onces end á que se ejecu ada obliga o iamen e, es deci , apa ece á en el esul ado. Es as ope aciones pueden se Ze oa ias, Una ias, Bina ias, Push o S o e. La lógica de cada una se á explicada pos e io men e. Pa a cada ipo de ope ación, el DZN inclui á una se ie de pa áme os. ●Núme o de ope aciones de ese ipo. Si e sob e odo pa a pode decla a los ec o es asociados co ec amen e. 19 ●Enume ados que ep esen an cada cómpu o del ipo co espondien e. Cada uno con iene la lis a de los nomb es de los cómpu os de ese ipo, a los cuales se iden i ica inequí ocamen e. ●A ays que con ienen los é minos de en ada y salida de ese ipo, siendo los é minos de en ada los elemen os que ese ipo de ope ación consume (desapilándolos) y los é minos de salida los que gene a (y añade a la cima de la pila) ese ipo de ope ación. La ope ación necesi a á que los é minos de en ada se encuen en en la cima pa a pode ejecu a se. El núme o de a ays depende á de las necesidades de ese ipo de ope ación. Po ejemplo, las ope aciones Ze oa ias (que no consumen ningún elemen o y p oducen un elemen o) sólo ienen un a ay llamado “ze oou ”; pe o las ope aciones Una ias (que consumen un elemen o y p oducen o o, ienen dos a ays) uno que con iene los é minos de en ada llamado “unin” y o o los de salida llamado “unou ”. ●A ay con el alo de gas pa a cada una de las ope aciones de ese ipo. ●A ay con el alo de size pa a cada una de las ope aciones de ese ipo. ●En caso de las ope aciones Bina ias, ambién end án un a ay de booleanos que indiquen si esa ope ación es conmu a i a o no. 4.2 Solución En la Figu a 4-2 se mues a un ejemplo de lo que con iene la solución de un p oblema conc e o. Se puede obse a cómo apa ecen las soluciones posibles po o den dec ecien e de cos e en unción de la unción obje i o especi icada, siendo la úl ima aquella que consigue la mayo op imización. Cada solución posible mues a lo siguien e: 20 ●Según el c i e io de op imización: el núme o de ins ucciones, el gas u ilizado o el size u ilizado. ●El a ay “ gas” que con iene el gas de cada ope ación asignada en ese es ado. ●El a ay “ size” que con iene el amaño de cada ope ación asignada en ese es ado. ●El a ay “p og am” que con iene las ope aciones a ejecu a de un es ado a o o, en el o den en el que se deben ejecu a . El a ay debe es a de inido con un amaño y ipo cons an es, lo que nos obliga a decla a lo con el amaño equi alen e a la can idad máxima de ins ucciones. Es o conlle a que a menudo el a ay no se llene en e o, sin emba go, debemos da les un alo a odas las posiciones. Po ello usamos Nop como ep esen ación de ninguna ope ación. ●La ma iz “s a es” de es ados de la pila, siendo la p ime a ila el es ado inicial y las siguien es ilas el es ado de la pila después de aplica la ope ación asignada en el es ado an e io . Es deci , la segunda ila mos a á el es ado de la pila una ez la p ime a ope ación ha sido ejecu ada, y así sucesi amen e has a llega al es ado inal de pila, que esul a de odas las ins ucciones ejecu adas. De mane a simila a Nop en el a ay “p og am”, es a ma iz incluye ambién espacios acíos o alo es “null”, ya que la ma iz se cons uye con un amaño ijo equi alen e al núme o máximo de es ados po el núme o máximo de elemen os en la pila. Así, cada ez que en un es ado la pila no es á llena, podemos e el alo ‘.’, que ambién o ma pa e del enume ado TERM de inido an e io men e. De es a mane a, podemos de ini “s a es” como una ma iz de ipo TERM pa a usa una ep esen ación aco de con MiniZinc. ●“Time elapsed” se e ie e al iempo que ha a dado MiniZinc en encon a dicha solución. 21 Figu a 4.2. Ejemplo de solución 4.3 Va iables y Cons an es Apa e de los da os in oducidos po el DZN ambién han sido necesa ias la decla ación de cie as cons an es, p incipalmen e pa a almacena alo es in e medios que pos e io men e se án u ilizados po alguna es icción. Se han c eado di e en es ins ancias de “se o in ” que ep esen an dis in os angos de acceso pa a nues os a ays y enume ados. Es os conjun os han sido muy ú iles a la ho a de eco e las es uc u as de la implemen ación, ya que apo an el ango de núme os en e los dos alo es deseados. Algunos de es os conjun os son los siguien es: ●SS: conjun o que ep esen a el ango [1, amaño del p og ama]. ●SN: conjun o que ep esen a el ango [1, amaño de la pila]. ●MDN: conjun o que ep esen a el ango [1, núme o de dependencias de memo ia]. Las a iables son los elemen os que o man la solución, de inidos en el comienzo de es e capí ulo. Además, en e las a iables ambién se encuen an los elemen os u ilizados pa a la op imización, explicada pos e io men e. 22 OPCODES es un ipo enume ado que se ha c eado pa a acili a el manejo de los códigos de ope ación. En la ejecución del p og ama exis en un núme o di e en e de ope aciones dis in as según el código a p ocesa , po es e mo i o es necesa ia una mane a de nomb a las den o del p opio código. Además, es impo an e de ca a a la decla ación del a ay “p og am”. Es e enume ado es á compues o po odos los enume ados de los di e en es ipos de ope aciones (“DUP_ENUM”, “SWAP_ENUM”, “ZEROARYOP”, “UNARYOP”, “BINARYOP”, “PUSHOP”, “STOROP”) jun o con las ope aciones Nop y Pop. Es o se ha podido ealiza g acias a que MiniZinc pe mi e ex ende los enume ados a a és de sus cons uc o es, de al o ma que se puede con e i un elemen o de un enume ado a o o usando la unción del cons uc o , llamada F, o su in e sa, llamada F^-1. El Enum OPCODES se decla a de la mane a usual en MiniZinc. Es inicializado igualándolo a la unión de los di e en es Enums que exis en en la implemen ación y, además, se añaden las ope aciones Nop y Pop. Pa a suma es os Enums se usa un cons uc o di e en e pa a cada Enum, que los ans o ma a ipo Opcodes. Cada una de es as unciones iene un nomb e dis in o. Aho a, Opcodes con iene una enume ación de odos los códigos de ope ación que se pueden u iliza pa a nues a solución. Figu a 4.3-1. Enume ado Opcodes Cuando se u iliza la unción F sob e el Enum o iginal, se e isa el con enido de ese Enum in e p e ándose como pa e de Opcodes. Es deci , la unción de uel e un alo de ipo Opcodes en ez del ipo del Enum o iginal. Cuando se u iliza la unción in e sa F^-1 sob e un alo de ipo Opcodes, de uel e el índice de ese alo en el Enum o iginal del cual p o iene. De es a mane a, 23 la unción in e sa pe mi e usa el índice sob e los a ays del ipo de ins ucción deseado. Un ejemplo se ía el siguien e: en la de inición an e io de OPCODES, SW(SWAP_ENUM) se u iliza pa a ep esen a los é minos del enume ado SWAP_ENUM como pa e de OPCODES. Es e mismo cons uc o se aplica a los é minos del enume ado inicial pa a c ea el é mino co espondien e en el enume ado ex endido. Po ejemplo, SWAP2 co esponde al alo en el enume ado SWAP_ENUM, y SW(SWAP2) se co esponde con el alo co espondien e en el enume ado de OPCODES. Con Opcodes lis o pa a su uso se puede u iliza como ipo pa a el a ay p og am, que con end á la solución inal. Sin Opcodes, la implemen ación cambia ía d ás icamen e, ya que pe mi e usa odas las ope aciones como un solo ipo y a la ez di e encia los sub ipos den o del enume ado, pudiendo dis ingui las es icciones adecuadas a cada ope ación conc e a. Figu a 4.3-2. A ay P og am El enume ado Opcodes es u ilizado en la mayo ía de las es icciones de di e sas o mas. 1. Iden i ica el ipo de ins ucción que se a a maneja . Al comienzo de cada es icción se comp ueba compa ando di ec amen e con una posición del de OPCODES (e.g. Nop, Pop) o comp obando si la ins ucción o ma pa e de uno de los Enums que o man OPCODES (po ejemplo, “DUP_ENUM”, “SWAP_ENUM”, e c.) Figu a 4.3-3. Iden i icación de ipo de ins ucción - Po posición 24 Figu a 4.3-4. Iden i icación de ipo de ins ucción - Po enum 2. Ob ene la posición que ocupa la ope ación en su Enum o iginal. Pa a pode accede a los da os de las ope aciones (pa áme os de en ada y salida, gas, size, e c.), se necesi a conoce su posición en el Enum o iginal, ya que el alo que se encuen a en el a ay p og am hace e e encia a su posición en Opcodes. Pa a ello, u ilizamos la unción in e sa. Figu a 4.3-5. Ob ención de la posición de una ins ucción 4.4 Pila Inicial y Final Pa a ga an iza la equi alencia en e la secuencia encon ada y la o iginal, la p ime a es icción de inida obliga a que el p ime es ado de la pila sea igual a “s a s ack” y el úl imo es ado de la pila sea igual a “ends ack”. Se implemen a de una mane a i e a i a, asegu ando que cada uno de los elemen os del p ime y del úl imo es ado son iguales a cada uno de los elemen os de los da os que se ienen sob e la en ada y la salida. Figu a 4.4. Res icción de p ime y úl imo es ado de la pila 4.5 Dependencias de Memo ia Se implemen an las dependencias de memo ia ya mencionadas pa a asegu a que los da os ob enidos en los accesos a memo ia son los co ec os y no han sido sob esc i os en un o den inadecuado. Es a in o mación se p opo ciona en el a chi o DZN en o ma de un ec o de duplas de ins ucciones en el que cada dupla 25 ep esen a una dependencia. Su signi icado es que una ez se ejecu a la segunda ope ación de la dupla, no se debe ejecu a la p ime a. Lo que quie e deci que, al ene la obligación de ejecu a odas las ope aciones p opo cionadas, la p ime a ope ación de la dupla debe ejecu a se obliga o iamen e an es que la segunda. Figu a 4.5. Res icción dependencias memo ia 4.6 Ope aciones de Pila En es a sección, se de ini án las es icciones que modelan el impac o de las ope aciones sob e la pila. Adicionalmen e, se de alla án las es icciones que se han c eado pa a sa is ace la ejecución de dichas ope aciones. 4.6.1 Ope ación Nop Nop es la “no ope ación”, es deci , cuando es e é mino apa ece en la solución es que en ese es ado no se ejecu a ninguna ope ación. Es a ope ación es necesa ia ya que nues o modelo ija un amaño máximo de ope aciones inicial y así se pueden encon a soluciones en las que se ejecu en menos ope aciones. Como se de alla an e io men e, el a ay solución debe asigna una ins ucción a cada posición y usamos Nop como “ elleno”. La es icción codi icada pa a modela es a ope ación obliga a que se cumplan dos condiciones cuando es aplicada en un de e minado es ado. 1. Las ope aciones en los es ados que es an deben se ambién Nop. Así e i amos di e en es e siones de una misma solución que solo di ie an en la posición de Nops. 2. En el siguien e es ado, la pila se debe man ene igual. 26 Asimismo, en la codi icación de la es icción se inco po a una condición que añada los alo es co espondien es de gas y size a los a ays de “ gas” y “ size”. La ope ación Nop iene alo es nulos pa a los c i e ios de gas y size. Figu a 4.6.1. Res icción Nop 4.6.2 Ope ación Pop Pop es una ope ación que desapila el p ime elemen o de la pila y lo desca a. Es a ope ación obliga a que se cumplan dos condiciones cuando es aplicada. 1. En el es ado sob e el cual se ejecu a, la p ime a posición de la pila no puede se igual al alo nulo, ya que la pila debe con ene al menos un elemen o. 2. En el siguien e es ado, al consumi el p ime elemen o, odos los elemen os de la pila a pa i del segundo se desplazan hacia la izquie da. Además, el úl imo elemen o se á igual al alo nulo po la necesidad de asigna un alo a cada posición de la ma iz. Asimismo, en la es icción se incluye una condición que añada los alo es co espondien es de gas y size a los a ays de “ gas” y “ size”. La ope ación Pop iene alo es ijos pa a gas y size de 2 y 1, espec i amen e. Figu a 4.6.2. Res icción Pop 27 Figu a 4.6.7. Res icción Bina ia 4.6.8 Ope aciones Push La ope ación Push inse a un elemen o en la p ime a posición de la pila. Se puede conside a un caso especial de ope ación Ze oa ia. Las conside amos en una ca ego ía di e en e po que son las únicas ins ucciones cuyo amaño en by es no es 1, sino que depende del alo que se in oduzca. Supe s ack [1] de ine es icciones adicionales especí icas pa a es as ope aciones, po lo que hemos decidido man ene las en una ca ego ía independien e. Es a ope ación se compo a como las ope aciones Ze oa ias. Figu a 4.6.8. Res icción Push 4.6.9 Ope aciones S o e S o e es la ope ación de inse ción en memo ia, que equie e los dos elemen os en la p ime a y segunda posición de la pila, pudiendo conside a la un caso especial de ope ación Bina ia sin elemen o de salida. En la codi icación de la es icción, p ime o, se iden i ica den o de su Enume ado asociado la posición de la ope ación 34 S o e que es á siendo analizada (x). Es a ope ación obliga a que se cumplan cie as condiciones cuando es aplicada en un de e minado es ado. 1. En ese es ado, el elemen o en la p ime a posición de la pila debe se igual al elemen o en la posición x en el a ay de “s o in1” y el elemen o en la segunda posición de la pila debe se igual al elemen o en la posición x en el a ay de “s o in2”. Es e ipo de ope ación no dispone de la opción de conmu a i idad ya que cada uno de los elemen os consumidos se usa á de mane a di e en e. 2. En el siguien e es ado, los elemen os en la úl ima y penúl ima posición de la pila deben se nulos, ya que dos elemen os han sido consumidos. 3. En el siguien e es ado, al habe consumido dos elemen os, odos los elemen os en la pila a pa i del e ce o se desplazan dos posiciones a la izquie da pa a e i a la apa ición de alo es nulos o inco ec os en la cima y subcima. La es icción sob e el gas y el amaño se aplica de la misma mane a que en las ope aciones Ze oa ias pe o u ilizando sus a ays co espondien es. Figu a 4.6.9. Res icción S o e 4.7 Res icciones Adicionales Finalmen e, se han añadido cie as es icciones pa a la op imización y pa a acili a al esolu o la búsqueda de soluciones. 35 4.7.1 Op imización La op imización iene un ol impo an e en la p og amación con es icciones, ya que es la o ma de que MiniZinc encuen e la solución más óp ima en unción de una unción obje i o especí ica. En el caso de es e p oyec o hemos incluido es c i e ios de op imización, codi icados de la o ma que mues a la Figu a 4.7.1-1. 1. El esolu o minimiza el núme o de ins ucciones en el p og ama. Como el amaño del a ay “p og am” es cons an e, es e c i e io es equi alen e a maximiza el núme o de Nops. Es a codi icación es mucho más sencilla y di ec a, po lo que se ha adap ado es a ep esen ación en nues o modelo. 2. El esolu o minimiza el gas o al u ilizado, es deci , la suma del gas que u iliza cada una de las ope aciones que o man pa e de nues a solución. 3. El esolu o minimiza el size o al u ilizado, es deci , la suma de size co espondien e a cada una de las ope aciones que o man pa e de nues a solución. Se elige un modo de op imización median e dos a iables, “op ion” oma alo es en e el 0 y el 2 de e minando cuál de las es opciones amos a usa . Po o o lado, ” alue” oma su alo dependiendo de “op ion”. Es e puede se el núme o de ope aciones, la suma de gas o la suma de size. Una ez elegido el alo pa a “ alue”, minimizamos su alo . En pa icula , pa a el núme o de ins ucciones minimizamos el núme o máximo de ope aciones menos el núme o de Nops. Figu a 4.7.1-1. Res icción Ze os, gas y size 36 Figu a 4.7.1-2. Minimización de alue 4.7.2 Fo za la Apa ición de Ope aciones Es a es icción obliga a que cada ope ación en los enums de “ZEROARYOP”, “UNARYOP”, “BINARYOP”, “STOROP” y “PUSHOP” apa ezcan en el p og ama. Es a es icción ayuda a eco a el espacio de soluciones y ejecu a más ápido ya que elimina odas las soluciones en las cuales no apa ezcan las ope aciones que ienen que se ejecu adas. Es a es icción es obliga o ia en el caso de ope aciones S o e, ya que en el caso con a io una solución puede p escindi de aplica las, al no gene a ningún elemen o de pila. Figu a 4.7.2. Res icción ope aciones 4.7.3 Cada Elemen o Usado Debe Se Inse ado Pa a eco a el espacio de búsqueda, es a es icción obliga a que cada elemen o p esen e en cualquie a de los a ays de los da os de en ada (“unin”, “binin1”, “binin2”, “s o in1”, “s o in2”) o en la pila de salida (“ends ack”), debe apa ece en la pila de en ada (“s a s ack”) o en los a ays de los da os de salida (“ze oou ”, “unou ”, “binou ”, “pushou ”). Es a condición se cumple sin necesidad de especi ica la es icción, sin emba go, aco a el iempo de ejecución ya que no conside a las soluciones que se ían desca adas más a de po inco ec as. La implemen ación pasa po comp oba uno a uno que cada elemen o de los a ays de en ada y pila inicial es á p esen e po lo menos en uno de los a ays de salida o pila inal. 37 Figu a 4.7.3. Res icción de elemen os usados e inse ados. 4.7.4 No In oduci Elemen os An es de una Ins ucción Pop Pa a eco a el espacio de búsqueda de ca a a la op imización, es a es icción obliga a no apila elemen os jus o an es de desca a los con una ins ucción pop. Si lle á amos a cabo al acción, end íamos en cuen a soluciones poco óp imas en las que el esul ado de una ope ación ca ece ía de u ilidad. Desca ando dichas soluciones a a és de es a es icción acele amos la búsqueda de secuencias más p ome edo as. La implemen ación de es a es icción consis e en comp oba que, si la ins ucción ac ual es Pop, la an e io debe se necesa iamen e Pop o Swap. Figu a 4.7.4. Res icción inse ción an es de Pop. 4.7.5 Limi a las ope aciones con cos e de gas mayo o igual que 3 Es a es icción busca gene a menos esul ados poco óp imos. Pa a no ob ene cos es en gas demasiado al os, las ope aciones que engan un cos e en gas mayo o igual que es pueden ejecu a se una sola ez. La implemen ación de la es icción eco e uno a uno el Enum de cada ipo de ins ucción. Pa a cada ins ucción comp ueba si su alo de gas es igual o mayo que es. Si es así, asegu a que es a ins ucción apa ezca en la solución como máximo una 38 ez. Es o esul a á siemp e en una apa ición si enemos en cuen a la es icción que de inimos en el apa ado 4.7.2. Figu a 4.7.5. Res icción al o cos e en gas 39 Capí ulo 5 - Expe imen ación En es a sección, e aluamos los mecanismos p opues os en el capí ulo 4 y en los Apéndices A y B sob e un conjun o signi ica i o de ejemplos, que co esponden a un subconjun o de los p og amas u ilizados en la e aluación expe imen al del a ículo de Supe S ack [1]: ●Una colección de 10 p og amas esc i os en Ci com de la biblio eca Ci com, un DSL pa a c ea ci cui os a i mé icos en p uebas de conocimien o-ce o. ●Una compilación de 10 con a os de código op imizados que ambién se emplea on en la e aluación de la he amien a de supe -op imización GASOL, p ecu so a de Supe S ack [1]. Los expe imen os se han ealizado en una máquina AMD Ryzen Th ead ippe PRO 3995WX, con 64 co es y 512 GB de memo ia, que ejecu a Debian 5.10.7. Los esul ados mos ados en es e capí ulo demues an que el modelo MiniZinc codi icado en es e p oyec o encuen a soluciones equi alen es pa a secuencias complejas en un iempo azonable. Es as secuencias habían sido op imizadas p e iamen e po sus espec i os compilado es, lo que demues a aún más el impac o de la écnica de supe -op imización. Las p uebas que se han ealizado han sido sob e las ex ensiones de es e p oyec o, explicadas en los dos apéndices. Se ha ejecu ado el modelo de MiniZinc c eado pa a EVM y Wasm pa a cada uno de los iche os de da os de ejemplo. U ilizando el comando “-- ime-limi ” de MiniZinc, se es ingió el iempo que podía a da el modelo en encon a una solución pa a cada ejemplo. Cuando el modelo a daba más de lo es ablecido, la ejecución se de enía, mos ando un mensaje simila al siguien e: 40 Figu a 5. Ejemplo de Timeou . Aunque se pa e la ejecución del modelo an es de que haya encon ado la solución óp ima, MiniZinc imp ime ambién las soluciones in e medias que ha encon ado. Es o es ú il pa a analiza cuán o iempo se a da en encon a cada solución mejo ada. Los da os se han ob enido ejecu ando sc ip s eu ilizados de Supe s ack [1] que se nos han p opo cionado pa a p ocesa los iche os de esul ados de los ejemplos. Es os sc ip s miden en e o as cosas el consumo en gas y size (en el caso de EVM) y el núme o de ins ucciones (en el caso de Wasm) pa a de e mina las ganancias co espondien es según el c i e io seleccionado, además de o a in o mación como, po ejemplo, el iempo de ejecución y si se ha conseguido p oba la op imalidad de la úl ima secuencia encon ada. También se ha eu ilizado un checke de Supe s ack [1] que ha comp obado que odas las soluciones encon adas son equi alen es a las de pa ida. En pa icula , se ha ex endido el checke pa a comp oba las condiciones de asocia i idad-conmu a i idad y ambién pa a la libe alización de las es icciones de la pila inal (es as ex ensiones se explican en el apéndice B). Todo el código que se ha u ilizado en es e TFG se puede encon a en es e eposi o io de Gi Hub: h ps://gi hub.com/beaaedo/ g. di.ucm.Aedo.Lopez-Mingo 5.1 Sc ip s adicionales Los siguien es sc ip s han sido c eados pa a ejecu a y p ocesa el modelo de MiniZinc con los di e en es p og amas analizados. 41 5.1.1 Con e sión de o ma o JSON a DZN Como se ha indicado p e iamen e, las secuencias a analiza se han p opo cionado en o ma o JSON. Pa a que MiniZinc uese capaz de p ocesa es os a chi os u ie on que se con e idos a un iche o de da os de MiniZinc o DZN. Pa a es e p oyec o han sido c eados dos sc ip s de Py hon, ambos con el mismo nomb e “dzn_gene a ion.py”, pe o en di e en es di ec o ios. Uno de los sc ip s p ocesa secuencias del lenguaje EVM y el o o de WebAssembly. En o ma son ela i amen e simila es, excep uando que ienen algunos pa áme os di e en es ya que ambos lenguajes necesi an di e en es conside aciones y ienen ipos de ope aciones di e en es. En es e sc ip , se eco en odos los campos del JSON p opo cionado y se imp imen las a iables co espondien es. Po ejemplo, como se puede e en la igu a 5.1.1, pa a gene a la pila inal o "ends ack", se c ea un a ay acío y se eco e el a ay de la pila inal ob enido del JSON, añadiendo los é minos al a ay acío. A con inuación, si la pila iene menos elemen os que su amaño máximo, se añaden elemen os nulos pa a ellena la. Po úl imo, se imp ime el a ay al iche o de da os de Minizinc en el o ma o "ends ack = [ Con enido del a ay ends ack ]". Figu a 5.1.1. Gene ación de la pila inal en “dzn_gene a ion.py”. 5.1.2 Sc ip s de Bash Con el in de simpli ica y aco a el p oceso de p uebas, ya que exis ían un núme o muy amplio de ejemplos que ejecu a ; se han c eado es sc ip s que 42 con ie an los ejemplos de JSON a DZN u ilizando el sc ip “dzn_gene a ion.py” co espondien e y, pos e io men e, ejecu en el modelo en MiniZinc u ilizando el iche o de da os. ●El sc ip “gene a _dzn.sh” in oca al sc ip “dzn_gene a ion.py” con odos los a chi os de ejemplos en o ma o JSON, uno a uno, y los almacena en un di ec o io llamado “ejemplos_dzn”. ●El sc ip “ejecu a _ejemplos.sh” in oca al sc ip de MiniZinc con odos los a chi os de ejemplos en o ma o DZN, uno a uno, y almacena el esul ado de la ejecución en un a chi o de ex o con el con enido de la solución, que pos e io men e gua da en un di ec o io llamado “ejemplos_ esul s”. Sepa a cada esul ado en un iche o de da os puede se ú il en el u u o pa a analiza los iempos de odas las secuencias in e medias. Como la ejecución de cada ejemplo es independien e, se ha podido pa aleliza la ejecución de las ins ancias u ilizando el comando “pa allel”. El comando GNU “pa allel” pe mi e ejecu a a ios comandos de o ma pa alela, especi icando la can idad de comandos con el pa áme o “-j núme o_de_comandos”. El uso de mecanismos de pa alelización ha pe mi ido acele a la e aluación expe imen al. Figu a 5.1.2. Uso de GNU Pa allel. ●Finalmen e, el sc ip “c ea dzn_ejecu a ejemplos.sh” ejecu a los dos sc ip s de inidos an e io men e. Es a es uc u a de sc ip s pe mi e desacopla el p oceso de gene ación de iche os de da os de MiniZinc de la ejecución de es os, lo cual ha acili ado la 43 Figu a 5.2.1-3. Da os de mejo a de aho o en ope aciones, gas y size con es icción adicional. El aho o de ope aciones ejecu adas es uno de los aspec os que “Mejo ada” no es capaz de mejo a , mien as que las o as con igu aciones sí lo hacen. Pa a aho a gas, a pesa de lo an e io y eniendo mejo as con odas las con igu aciones, “Mejo ada” es la mejo opción. Es e esul ado se uel e a epe i cuando se cuan i ica el aho o en size. Con los esul ados ob enidos podemos asegu a que la mejo combinación global es “Mejo ada”, ya que supe a a “Cima_pila” indi idualmen e y a “Todo” en la mayo ía de los casos. 5.2.2 Nue as Ex ensiones - Aplanamien o O a de las ex ensiones que se ha ealizado sob e el modelo de EVM es la in oducción de la p opiedad asocia i a como o ma de encon a soluciones, la cual se á explicada en el Apéndice B. Una ez conocida la mejo combinación de 50 es icciones has a aho a (“Mejo ada”), se aplica el aplanamien o o asocia i idad ac i ando es as es icciones pa a obse a las mejo as que apa ecen. Figu a 5.2.2-1. Da os de mejo a de soluciones encon adas po asocia i idad. Se puede e cla amen e que la asocia i idad no p esen a mejo as a la ho a de encon a soluciones, independien emen e del es ilo de minimización elegido. 51 Figu a 5.2.2-2. Da os de mejo a en iempo de ejecución po asocia i idad. El iempo de ejecución se e educido siemp e que no se minimice size, pe o la di e encia es ealmen e pequeña. Figu a 5.2.2-3. Da os de mejo a de aho o en ope aciones, gas y size po asocia i idad. En el caso del aho o, ya sea en núme o de ope aciones, gas o size, se en esul ados muy simila es pa a ambas con igu aciones. Se obse a que es as di e encias an pequeñas (o incluso nulas) se deben a que el con enido del da ase no explo a lo su icien e la asocia i idad. De 7483 bloques que se usan como ejemplo, an solo se aplanan 133, que es una can idad ela i amen e pequeña. Se usa á un nue o conjun o de da os pa a comp oba el impac o eal de la asocia i idad o aplanamien o. Pa a ello, cons uimos 5000 secuencias alea o ias que aplican asocia i idad o aplanamien o. Es as secuencias se han gene ado siguiendo el siguien e p ocedimien o: 52 ●Se gene an secuencias alea o ias de “OPCODES” de un conjun o especí ico (ADD, MUL, PUSH 1, SUB, MSTORE, MLOAD, SWAP1, SWAP2, SWAP3, DUP1, DUP2, DUP3. A ADD y MUL). A las ope aciones conmu a i as del conjun o se les asocia el iple de p obabilidad de apa ece en las secuencias pa a que así se ienda a eu iliza cómpu os conmu a i os al e nando o as ope aciones. ●Se seleccionan las secuencias que con ienen al menos un aplanamien o y cinco como máximo has a consegui 5000 ejemplos. En las g á icas se pueden e los da os p oceden es del nue o da ase donde “AC_Gas” ep esen a los cambios que e ec úa la asocia i idad cuando se minimiza gas y “AC_Size” cuando se minimiza size. “No_AC_Gas” y “No_AC_Size” ep esen an la ejecución del mismo da ase sin usa asocia i idad. Figu a 5.2.2-4. Da os de mejo a en po cen aje de soluciones encon adas po asocia i idad - Nue o Da ase . Po desg acia, la asocia i idad pa ece empeo a el po cen aje de soluciones encon adas ap oximadamen e en un 3.5% pa a minimizaciones de gas y size. 53 Figu a 5.2.2-5. Da os de mejo a en iempo de ejecución (s) po asocia i idad - Nue o Da ase . Sin emba go, el iempo de ejecución sí se educe y de mane a más impo an e que con el an iguo conjun o de da os. La educción es de una magni ud pa ecida en e un c i e io de minimización y o o. 54 Figu a 5.2.2-6. Da os de mejo a en aho o en gas y size encon adas po asocia i idad - Nue o Da ase . El aho o an o en gas como en size se uel e e iden e pa a es e conjun o de da os. Es e conjun o de secuencias demues a que es a ex ensión mejo a el modelo en iempo de ejecución y aho o de gas y size, siemp e y cuando se aplique aplanamien o de o ma ex ensi a. 5.2.3 Nue as Ex ensiones - Libe alización de pila La úl ima ex ensión que se ha in oducido sob e el modelo de EVM es la libe alización de la pila inal. Es deci , el es ado de pila inal debe con ene el mismo conjun o de elemen os que la pila inal dada po el p oblema, pe o no necesa iamen e en el mismo o den. La libe alización de la pila se á explicada en el Apéndice B. Pa a e alua es a ex ensión se han gene ado es icciones alea o ias de pila sob e la colección de pa ida. Se han il ado los bloques que enían 3 o más elemen os en la pila inal, ya que es el mínimo que hace al a pa a que cob e sen ido la libe alización. Sob e es e g upo il ado, se ha gene ado un núme o alea o io de es icciones de o den de la pila inal (como máximo el núme o de elemen os de es a - 2). Las es icciones se gene an seleccionando dos elemen os alea o ios de la pila inal, o zando a que se man enga la di e encia de posiciones exis en e en e ellos. Así se ha asegu ado la ac ibilidad del p oblema, ya que po cons ucción la secuencia o iginal cumple las es icciones. El nue o conjun o de da os cons a de 3087 secuencias de ins ucciones. En las siguien es g á icas se mues an cua o ejecuciones dis in as. “Mejo ada” es la ejecución ob enida de los expe imen os an e io es usando las es icciones “Pop” 55 y “Cima_pila”. “No mal” ep esen a una combinación de las mismas es icciones sob e el nue o conjun o de da os. “Con ig” indica los da os ob enidos al añadi la libe alización de pila y “Con ig_AC” incluye además aplanamien o. Figu a 5.2.3-1. Da os de mejo a en po cen aje de soluciones encon adas po libe alización de pila. La libe alización añade soluciones encon adas cuando se minimiza Gas, quedando el alo pa a minimización de size lige amen e po debajo que el de “No mal”. Como eíamos en el apa ado an e io , la inclusión de asocia i idad no a o ece a la búsqueda de soluciones. 56 Figu a 5.2.3-2. Da os de mejo a en iempo de ejecución (s) po libe alización de pila. Se ob ienen unos da os sa is ac o ios pa a la educción del iempo de ejecución, an o la libe alización como la libe alización con asocia i idad lo educen de mane a isible pa a cualquie c i e io de minimización. 57 Figu a 5.2.3-3. Da os de mejo a en aho o en gas y size encon adas po asocia i idad. Pa a e mina , no se en cambios signi ica i os pa a el aho o de gas y size, aunque pa a la minimización de size se en pequeños inc emen os de aho o con libe alización de pila, an o con asocia i idad como sin ella. Se concluye que la libe alización de la pila es ú il p incipalmen e pa a educi el iempo de ejecución de los ejemplos, pe o su combinación con asocia i idad no p oduce mejo as ex as. 5.3 Wasm El da ase u ilizado pa a WebAssembly con iene 2256 ejemplos con secuencias de ins ucciones de amaño en e 1 y 20. Hemos op imizado es os ejemplos usando di e en es imeou s. Dado que en Wasm no había que e alua di e en es ex ensiones ni di e en es c i e ios de op imización (como en EVM), se ha decidido e alua cómo a ec an di e en es imeou s a las soluciones encon adas. Se ha ejecu ado el modelo 58 de MiniZinc pa a Wasm u ilizando es lími es de iempo di e en es: 180 segundos, 300 segundos y 420 segundos. El a io de núme o de soluciones encon adas y iempo lími e u ilizado es el espe ado. Cuan o más iempo se pe mi e ejecu a cada ejemplo, más soluciones encuen a, como se puede e en la siguien e igu a. También es necesa io pun ualiza que los ejemplos en los cuales no se ha encon ado solución, independien emen e del iempo lími e, con ienen odos 20 ins ucciones a op imiza . Es deci , pa a ejemplos con un código de 16 ins ucciones o menos a op imiza , encuen a una solución op imizada a odos. Figu a 5.3-1. G á ico de Núme o de Ejemplos s. Núme o de Soluciones Encon adas. En cambio, cuan o más al o sea el iempo lími e mayo es la media geomé ica de ope aciones op imizadas, siendo es as el núme o de ope aciones que con iene cada solución op imizada. Es o se puede explica ácilmen e eco dando que, los únicos ejemplos a los cuales no ha encon ado solución son los que con ienen 20 59 debido a es icciones de iempo, el modelo que inco po a es a ges ión de sime ías no ha encon ado esul ados du an e la expe imen ación pa a un conjun o signi ica i o de ejemplos, ap oximadamen e pa a el 40% de los ejemplos o ales. El obje i o de implemen a una es icción nue a que eduje a más aún la búsqueda se ha cumplido. Los expe imen os han demos ado que la es icción ela i a a las ins ucciones que se pueden habe ejecu ado pa a llega a una pila con cima X, jun o con la ela i a a las ins ucciones que se pueden ejecu a an es de una ope ación Pop, es la que ha dado luga a una mayo op imización. Po desg acia, la combinación de es as es icciones no consigue mejo a el aho o de ope aciones ejecu adas. El sopo e de la asocia i idad en ope aciones bina ias se ha implemen ado exi osamen e. Sin emba go, no consigue el obje i o de aumen a el núme o de soluciones encon adas. Es o hace que se plan ee la posibilidad de limi a la can idad de ejemplos en el conjun o de da os en los que se puede aplica asocia i idad pa a encon a más soluciones mien as se op imizan iempo de ejecución, núme o de ope aciones, gas y size. La libe alización de la pila de salida ambién se ha implemen ado de mane a co ec a dando unos esul ados especialmen e buenos a la ho a de educi el iempo de ejecución. Se ía in e esan e isi a la idea de libe aliza la pila de en ada de una mane a pa ecida a la que se ha ealizado. 66 Capí ulo 7 - Conclusions and u u e wo k As i has been de ined in he in oduc ion o his documen , he objec i es o his p ojec we e o model wi h MiniZinc he p oblem o au oma ically gene a ing op imized agmen s o low-le el code o EVM, based on wha had al eady been modeled by Supe s ack [1], modeling his same p oblem o Wasm and, inally, he implemen a ion o new ex ensions o he EVM model, including a cons ain wi h he objec i e o educing e en mo e he sea ch in op imiza ion, implemen a ion o associa i i y and s ack libe aliza ion. The i s objec i e, o model he supe -op imize p oposed by Supe s ack [1] in Minizinc, has been success ully achie ed. We ha e been able o success ully model all he cons ain s p oposed by Supe s ack [1] and “Supe op imiza ion o Sma Con ac s” [2] and a solu ion was ound o he examples wi h which he model was es ed. In his p ocess, a cons ain was implemen ed (sec ion 4.7.4), modeled be o e by [2], ha p o ided a good imp o emen in inding solu ions, execu ion ime, ope a ion sa ing, gas sa ing and size sa ing wi h any o he h ee minimiza ion ypes. In ega d o he model de eloped o op imize blocks o code w i en in he language WebAssembly, e en hough good esul s ha e been ob ained du ing he expe imen a ion phase, i would be bene icial o con inue explo ing di e en execu ion ime limi s. This would allow us o con i m ha he model can ind solu ions o he leng hies blocks o code. Also, a s a egy ha has no been success ully p o ed is he implemen a ion o symme y con ol cons ain s. This echnique sea ches o a oid he execu ion o edundan ope a ions wi h egis e s, es ic ing he equency and momen o occu ence o Se X and TeeX ope a ions. Howe e , due o ime es ic ions, he model 67 ha inco po a es his has no ound solu ions du ing expe imen a ion o a g ea e numbe o examples, app oxima ely 40% o he o al numbe o examples. The goal o implemen ing a new cons ain ha could educe he sea ch e en mo e has been achie ed. Expe imen s demons a ed ha he cons ain conce ning ope a ions ha can be execu ed o ge o a s ack wi h x a he op, as well as he one conce ning ope a ions ha can be execu ed be o e a POP ope a ion, is he one ha led o a bigge op imiza ion, especially in ce ain condi ions. Sadly, he combina ion o hese wo cons ain s do no add up o ope a ion sa ing. Associa i i y suppo in bina y ope a ions has been implemen ed success ully. Ne e heless, i does no achie e he objec i e o inc easing he numbe o ound solu ions. This can be a eason o conside he possibili y o educing he quan i y o examples in he da ase in which associa i i y can be applied so mo e solu ions can be ound while execu ion ime, ope a ion numbe , gas and size a e op imized. Final s ack libe aliza ion has also been implemen ed co ec ly leading o especially good esul s when educing execu ion ime. I could be in e es ing o isi he idea o libe alizing he ini ial s ack in a simila way o wha has been done. 68 CONTRIBUCIONES PERSONALES Apéndice A - Apo aciones de Bea iz Aedo Diaz. WebAssembly. Uno de los e os p opues os ha sido la implemen ación de un modelo de MiniZinc pa a la op imización de secuencias de código en WebAssembly. Es o ha supues o cambios signi ica i os en el modelo. La mayo di e encia en e el modelo de EVM y Wasm es la in oducción de egis os. Es e compo amien o se ha modelado añadiendo una ma iz con los es ados de cada egis o. Figu a A-1. Solución Wasm. Cambios en Cons an es y Va iables Con la in oducción de la manipulación de egis os hay cons an es que se han eliminado y o as que se han añadido. Las que se han eliminado son las siguien es. 69 ●Todas las cons an es pa a los ipos de ope ación Ze oa ias, Una ias, Bina ias, Push y S o e han sido eliminadas ya que, en es e modelo, la clasi icación en unción de la a idad de las ope aciones ha sido eliminada pa a Wasm. Wasm no iene cinco ipos de ope aciones de inidas, sino que iene ope aciones que pueden consumi de 0-3 a iables de en adas y pueden p oduci de 0-3 a iables de salidas. Po lo que, al se an a iable, no iene sen ido ene las ope aciones de inidas po núme o de en adas y salidas. ●Los enume ado es de las ope aciones DupX y SwapX ya que no son ope aciones que exis an en es e lenguaje. Además, las cons an es que se han añadido pa a la ges ión de egis os son las siguien es. ●El en e o 'NR' con iene el núme o de egis os a los cuales se an a aplica cambios. ●El “max_ egis e s_sz” con iene el núme o máximo de egis os adicionales que pueden se u ilizados. Es os egis os adicionales son ú iles pa a pode gua da cómpu os in e medios y así eu iliza los, pudiendo esul a en una mayo op imización. ●El a ay “ egis e _changes” con iene el es ado inicial y inal que deben ene los egis os. Los alo es que es án almacenados den o de los egis os pe enecen al enume ado TERM. Se ha de inido una nue a a iable, añadida en la solución, llamada “ egis e _s a es”. Es a a iable almacena el con enido de los egis os en cada es ado del p og ama. 70 Al no habe de inido las ope aciones en Wasm po ipos, odas las cons an es de inidas pa a las ope aciones son comunes pa a odas ellas. Son las siguien es: ●El enume ado “OP” ep esen a cada cómpu o. ●El en e o “N” es igual al núme o de cómpu os. ●Dos en e os “in_ops” y “ou _ops” con el núme o de pa áme os de en ada que consume y el núme o de pa áme os de salida que p oduce cada ope ación, espec i amen e. ●A ays con los pa áme os de en ada que consume (llamados “in1”, “in2” e “in3”) y el núme o de pa áme os de salida (llamados “ou 1”, “ou 2” e “ou 3”) que p oduce cada ope ación. No odas las ope aciones consumen y p oducen es pa áme os po lo que el a ay con end á los é minos co espondien es que consume y p oduce y asigna á elemen os nulos pa a indica que no p oduce ni consume ningún elemen o. ●A ay “comm” o mado po booleanos que indican si la ope ación co espondien e es conmu a i a. O o cambio impo an e es que el concep o de gas no exis e en Wasm ya que es una mé ica de la EVM. El concep o de size si exis e en Wasm pe o no es de in e és es udia lo. Po an o, se ha que ido es udia la supe -op imización del núme o de ins ucciones. Po lo que, aunque los a ays de gas y size siguen de inidos en el modelo pa a p ese a el modelo an e io , han sido igualados a uno en odos los casos. También se han añadido es ipos de ope aciones de manipulación de egis os nue as en Wasm, que no exis ían pa a EVM, ya que es e es el mecanismo u ilizado en es e lenguaje pa a ges iona la pila. Las ope aciones son Se X, Ge X y TeeX, cuyo uncionamien o se á explicado más adelan e. De o ma simila a DupX y SwapX en EVM, se in oducen como cons an es es enume ados con los Se X, Ge X y TeeX que se 71 pueden ealiza . Las es icciones c eadas en el modelo de EVM pa a la ges ión de las ope aciones DupX y SwapX ambién han sido eliminadas. Al habe cambiado la o ma en la que se de inen las ope aciones, el enume ado OPCODES ambién ha cambiado. Aho a OPCODES es á compues o po odos los enume ados de “SET_ENUM”, “GET_ENUM”, “TEE_ENUM” y “OP” jun o con las ope aciones Nop y Pop. Figu a A-2. Enume ado OPCODES en Wasm. Finalmen e, se han de inido dos se s o in nue os. Un conjun o llamado RN que ep esen e el ango [1, NR + max_ egis e s_sz], es deci , que ep esen e odas las posiciones de los egis os. Y o o llamado NR1 que ep esen e el ango [1, NR + 1], es deci , que ep esen e las posiciones de los egis os que ienen que su i modi icaciones. Ope aciones con Regis os A con inuación, se an a explica más en de alle el uncionamien o de las es ope aciones de manipulación de egis os nue as en Wasm. ●Se X: es a ope ación consume el p ime elemen o de la pila y lo in oduce en el egis o X. Se in oduce una ope ación Se X po cada egis o disponible. Figu a A-3. Ope ación Se X 72 ●Ge X: es a ope ación in oduce en la cima de la pila el alo que es é almacenado en el egis o X. Se in oduce una ope ación Ge X po cada egis o disponible. Figu a A-4. Ope ación Ge X ●TeeX: es a ope ación, en la que X se e ie e al núme o de egis os en los que puede ealiza se, in oduce el p ime elemen o de la pila en el egis o X sin consumi lo. Figu a A-5. Ope ación TeeX Adicionalmen e, se han añadido es icciones pa a la ges ión de los egis os, que son bas an e simila es a las es icciones de ges ión de la pila. ●En el es ado inicial y inal de los egis os se co esponde con el de inido en el a ay de “ egis e _s a es”. ●Los egis os adicionales inicialmen e no deben con ene nada, es deci , con ienen el alo nulo. Figu a A-6. Res icciones de ges ión de egis os Las ope aciones de Nop y Pop se han man enido iguales, sal o que se ha añadido una condición en ambas pa a que los egis os en el siguien e es ado se man engan igual que en el es ado en el que se aplica la ope ación. 73 Figu a A-7. Ope aciones Nop y Pop en Wasm. Po úl imo, se ha añadido una es icción que man iene el mismo alo en los egis os después de ope aciones que pe enezcan al enume ado OP, ya que esas ope aciones no ealizan modi icaciones en los egis os. Figu a A-8. Res icciones de ope aciones no de egis os Ope aciones sob e la Pila Como se ha comen ado an e io men e, o o de los cambios espec o a EVM es que la clasi icación en unción de la a idad de las ope aciones ha sido eliminada pa a Wasm. Es o ambién ha cambiado adicalmen e la o ma de de ini las es icciones de las ope aciones en MiniZinc. Aho a hay de inidas cua o es icciones pa a la ges ión de ope aciones. Si una ope ación es conmu a i a en onces unciona á igual que una ope ación Bina ia conmu a i a en EVM, consumiendo dos elemen os y gene ando uno. Figu a A-9. Res icción Wasm pa a los pa áme os de en ada. Conmu a i as. 74 Si una ope ación no es conmu a i a en onces consumi á el núme o de pa áme os de en ada que enga que es én en la cima de la pila en ese es ado. Figu a A-10. Res icción Wasm pa a los pa áme os de en ada. No conmu a i as. Todas las ope aciones, dependiendo de la can idad de pa áme os de salida, in oduci án los pa áme os de salida que engan en la cima de la pila en el es ado siguien e. Figu a A-11. Res icción Wasm pa a los pa áme os de salida. Todas las ope aciones, además, obligan que se cumplan cie as condiciones e e en es al es ado de los elemen os de la pila que no han sido modi icados po la ope ación. La es icción se impone dependiendo de la di e encia en e el núme o de pa áme os de salida y de en ada. ●Si el núme o de pa áme os de salida es mayo que el de en ada. 1. En el siguien e es ado, los elemen os desde el que es á en la posición que sigue al núme o de pa áme os de salida has a el úl imo son iguales al elemen o que es é en esa posición menos la es a del núme o de pa áme os de salida menos los de en ada. 2. Los elemen os en ese es ado en las posiciones úl imas, co espondien es con la di e encia en e los pa áme os de salida y en ada, deben se nulos. 75 Figu a B-4. Res icción ASSOCIATIVEADDOP. Libe alización de la Pila Final En la e sión o iginal de la codi icación pa a EVM las pilas de en ada y salida son ijas. Es deci , pa a sa is ace el p oblema se debe llega a una solución cuyo p ime es ado de pila sea exac amen e igual que la pila de en ada y el úl imo es ado exac amen e igual que la pila de salida. En es a ex ensión, se elaja es a condición undamen al pa a el p oceso de supe -op imización pa a así explo a secuencias que no son exac amen e equi alen es a las de pa ida, pe o que ealizan los mismos cómpu os. Se in oduce el concep o de la libe alización de la pila inal. Es o quie e deci que el es ado de pila inal debe con ene el mismo conjun o de elemen os que la pila inal dada po el p oblema, pe o no necesa iamen e en el mismo o den. Es a ex ensión a a de mejo a el código en el con ex o del p og ama del que ha sido ex aído, explo ando dis in os ó denes en los elemen os de la pila cuando se alcanzan los bloques suceso es del CFG. Pa a asegu a que la pila inal sigue siendo álida pa a su uso en el siguien e bloque se imponen unas condiciones que limi an la libe alización. Las es icciones que se imponen sob e la pila de salida ep esen an la posición ela i a de un elemen o espec o a o o. Conc e amen e se indica la dis ancia que hay en e ambos de la siguien e mane a. Recibimos una upla con es a o ma: (S_i, S_j, k) 82 Que nos da la siguien e in o mación: Pos(S_i) + k <= Pos(S_j) Donde Pos(x) es la posición del elemen o de ipo “TERM” en la pila inal. Pa a la implemen ación en MiniZinc seguimos a ios pasos: ●Modi icamos el sc ip “dzn_gene a ion.py”. Se añade la opción de que el a chi o JSON a lee con enga un campo “o de _ g _ws”. Si el JSON no con iene dicho campo signi ica que la ejecución se á como has a aho a, si es á p esen e pe o es acío se inco po a á libe alización de pila sin dependencias y si encon amos un campo “o de _ g _ws” con con enido se end án en cuen a las dependencias pa a la libe alización. El sc ip además esc ibi á sob e el DZN las nue as cons an es necesa ias decla adas en MiniZinc. ●Se incluyen nue as cons an es a la codi icación de MiniZinc: el Booleano “lib” indica si se aplica á libe alización o no, el en e o “nlib” ep esen a el núme o de dependencias (0 si lib = alse), el a ay “lib_elem” con iene una pa eja de elemen os po dependencia que mues an los elemen os sob e los que aplica la dependencia (S_i y S_j) y po úl imo el a ay “lib_dis” con iene el alo “k” que conc e a la dis ancia en e elemen os. Figu a B-5. Cons an es pa a libe alización. ●Se modi ica la es icción ela i a a la pila de en ada pa a usa la únicamen e en caso de no aplica libe alización. Aho a la ejecución de la es icción es á condicionada po la cons an e “lib”. 83 Figu a B-6. Cambio de es icción pila de salida. ●Se ag ega una nue a es icción pa a la pila inal que cub e el caso “lib” = ue. Es a es icción consis e en comp oba que cada elemen o exis en e apa ece el mismo núme o de eces en la pila inal dada po el p oblema y la pila inal del esul ado. Con es o se indica que la pila inal gene ada es á compues a del mismo conjun o de elemen os que la pila inal que se ecibió como da o de en ada. Figu a B-7. Res icción de pila de salida con libe alización. ●Se codi ica una es icción adicional que implemen a las posiciones ela i as en e elemen os de la pila inal. Pa a ello, se de inen dos a iables a y b que ep esen an las posiciones de S_i y S_j. Se buscan alo es que pueden oma a y b de al mane a que la posición a de la pila inal sea S_i (lib_elem[i,1]) y la posición b sea S_j (lib_elem[i,2]). Los alo es encon ados pa a a y b se usan en la condición ya explicada: {a + lib_dis[i] <= b donde lib_dis[i] ep esen a el alo k}. Es a comp obación se epi e pa a odas las condiciones que exis an espec o a las posiciones de la pila inal (un o al de nlib). Figu a B-8. Res icción libe alización con condiciones. 84 BIBLIOGRAFÍA [1] Albe , E., Ga cia de la Banda, M., He nández-Ce ezo, A., Igna ie , A., Rubio, A., & S uckley, P. J. (2024, Junio). Supe S ack: Supe op imiza ion o S ack-By ecode ia G eedy, Cons ain -Based, and SAT Techniques. ACM P og am,Lang. 8, PLDI(A ículo 205), 26 páginas. h ps://doi.o g/10.1145/3656435 [2] Albe , E., Go dillo, P., He nández-Ce ezo, A., Rubio, A., & Sche , M. A. (2022, Julio). Supe op imiza ion o Sma Con ac s. ACM T ans,So w. Eng. Me hodol. 31, 4, 70, 29 páginas. h ps://doi.o g/10.1145/3506800 [3] Ap , K. (2003). P inciples o cons ain p og amming. Camb idge Uni e si y P ess. h ps://books.google.es/books?id=1e7Ib04 ZAcC&lpg=PR11&dq=%20P inciples%2 0o %20Cons ain %20P og amming&l &hl=es&pg=PR2# =onepage&q=isbn& = al se [4] Chu, G., S uckey, P. J., Schu , A., Ehle s, T., Gange, G., & F ancis, K. (2015). Chu ed, a lazy clause gene a ion sol e . Gi Hub. Re ie ed May 20, 2024, om h ps://gi hub.com/chu ed/chu ed? ab= eadme-o - ile [5] Hols Swende, M., Bylica, P., Be egszaszi, A., & Maibo oda, A. (2021, Julio). EIP-3860: Limi and me e ini code. E he eum Imp o emen P oposals, (no. 3860). h ps://eips.e he eum.o g/EIPS/eip-3860 85 [6] Sa aswa , V., & Van Hen en yck, P. (1995). P inciples and P ac ice o Cons ain P og amming: The Newpo Pape s (V. Sa aswa & P. Van Hen en yck, Eds.; Vol. MiniZinc: Towa ds a S anda d CP Modelling Language). Ne Lib a y, Inco po a ed. [7] The Solidi y Au ho s & e he eum.o g. (2016). In oduc ion o Sma Con ac s — Solidi y 0.8.27 documen a ion. Solidi y Documen a ion. Re ie ed May 24, 2024, om h ps://docs.solidi ylang.o g/en/la es /in oduc ion- o-sma -con ac s.h ml [8] S uckey, P. J., Ma io , K., & Tac, G. (2020). Speci ica ion o MiniZinc. Minizinc. Re ie ed May 20, 2024, om h ps://www.minizinc.o g/doc-2.8.4/en/spec.h ml [9] WebAssembly Communi y G oup & Rossbe g, A. (2024, 4 28). WebAssembly Speci ica ion. Re ie ed May 20, 2024, om h ps://webassembly.gi hub.io/gc/co e/_download/WebAssembly.pd [10] Wood, G. (2014). E he eum: A secu e decen alised gene alised ansac ion ledge . h ps://e he eum.gi hub.io/yellowpape /pape .pd . h ps://e he eum.gi hub.io/yellowpape /pape .pd 86