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