García Sánchez, Carlosde la Calle Montilla, Enrique2023-11-022023-11-022023https://hdl.handle.net/20.500.14352/88539Trabajo de Fin de Máster en Métodos Formales en Ingeniería Informática, Facultad de Informática de UCM, Departamento de Arquitectura de Computadores y Automática, Curso 2022/2023. The final result is a fully working rendering engine available in the https://github.com/101001000/ElevenRender repositoryThis work covers the development, implementation, and analysis of Eleven Render, an architecture-independent photo-realistic rendering engine. It is written in C++ and utilizes the SYCL programming model which allows code to run in a vast range of heterogeneous architectures like: CPUs, GPUs, and FPGAs, bestowing upon Eleven Render, with a portability level rarely seen in other engines, and making it one of the first SYCL rendering engine implementations. A new shading language called ASL has been formally specified and implemented in Coq. Making use of Coq’s verification tools and the Vellvm project, which endows LLVM-IR of a formally specified semantics, a semantic-preserving translator from ASL to LLVM-IR has been implemented and verified. The resulting LLVM-IR shader code is then fed to the Intel’s SYCL implementation DPC++, and is compiled to the desired target architecture. The entire process has been evaluated and benchmarked in different architectures.Este trabajo cubre el desarrollo, la implementación y análisis de Eleven Render, un motor de renderizado fotorrealista independiente de plataformas de hardware. Está hecho en C++ y hace uso del modelo de programación de SYCL, que permite ejecutar código en un gran abanico de arquitecturas heterogéneas, tales como: CPUs, GPUs y FPGAs, dotando a Eleven Render, de una portabilidad raramente vista en otros motores, y siendo así una de las primeras implementaciones en SYCL de motor gráfico fotorrealista. Se ha propuesto también un nuevo lenguaje de shading llamado ASL, que ha sido formalmente especificado e implementado en Coq. Haciendo uso de las herramientas de verificación de Coq y el proyecto Vellvm, que dota al lenguaje LLVM-IR de una semántica formalmente especificada, se ha implementado y verificado un traductor de ASL a LLVM-IR. El código resultante de dicha traducción, es entonces incluido en el proceso de compilación llevado a cabo por la implementación de SYCL hecha por Intel: DPC++. Todo este proceso ha sido posteriormente evaluado y sometido a pruebas de rendimiento en diferentes arquitecturas de hardware.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/master thesishttps://github.com/101001000/ElevenRenderopen access004(043.3)Render 3DSYCLDPC++Path TracingRay TracingCoqVellvmASLTrazado de RayosInformática (Informática)33 Ciencias Tecnológicas