El Portal de las Tecnologías para la Innovación

Microsoft en SOSP 2024: Innovaciones en investigación de sistemas

Microsoft se enorgullece de patrocinar el 30.º Simposio sobre Principios de Sistemas Operativos ( SOSP 2024), lo que pone de relieve su compromiso con el avance de la investigación en sistemas informáticos. 

En una época en la que la infraestructura digital sustenta casi todas las facetas de la vida moderna, SOSP sirve como un foro importante para mostrar las tecnologías que dan forma a nuestro mundo interconectado. Organizado anualmente por la Association for Computing Machinery (ACM), el simposio reúne a expertos para explorar las innovaciones en sistemas operativos, sistemas distribuidos y software de sistemas.

Con siete artículos aceptados, incluido “ Verus: A Practical Foundation for Systems Verification ”, que ganó el premio Distinguished Artifact Award, así como dos talleres y un tutorial, los investigadores de Microsoft presentan un trabajo innovador que fortalece la seguridad, la eficiencia y la escalabilidad de la computación en la nube y los sistemas distribuidos. Este trabajo no solo contribuye al conocimiento teórico, sino que también aborda desafíos del mundo real, ayudando a garantizar que, a medida que los sistemas informáticos se vuelven más complejos, sigan siendo sostenibles, confiables y seguros.

Continúe leyendo para obtener más información sobre las contribuciones de Microsoft a SOSP 2024, incluidos los avances que abordan las demandas cambiantes de la informática moderna.

Papeles

Reproducción eficiente de fallas inducidas por fallas en sistemas distribuidos con inyección de fallas impulsada por retroalimentación

Jia Pan, Haoze Wu, Tanakorn Leesatapornwongsa , Suman Nath , Peng Huang

Diagrama de la arquitectura y el flujo de trabajo de Anduril. Anduril contiene dos componentes principales, Instrumenter y Explorer. Instrumenter recibe el código de bytes del sistema y el archivo de registro de fallas de producción. Realiza un análisis estático y calcula un gráfico causal que consta de puntos del programa potencialmente relacionados con el síntoma de falla. Además, inserta fragmentos de código en el sistema para (1) inyectar una falla para generar una excepción deseada y (2) registrar información adicional para facilitar los algoritmos de retroalimentación. Tenga en cuenta que Anduril no instrumenta el sistema de producción. Su registro de fallas de entrada proviene del sistema no instrumentado.

Esta investigación presenta Anduril, una técnica de inyección de fallas que reproduce rápidamente fallas específicas inducidas por fallas en sistemas de producción. Anduril utiliza un análisis causal estático y un novedoso algoritmo impulsado por retroalimentación para buscar rápidamente en el espacio de fallas la causa y el momento en que se produjo la falla. La evaluación de 22 fallas inducidas por fallas reales de cinco sistemas distribuidos a gran escala demuestra la capacidad de FIR para reproducir todas las fallas al identificar e inyectar las fallas de causa raíz en el momento correcto.


Si no tiene éxito a la primera, inténtelo, inténtelo de nuevo… Perspectivas y herramientas basadas en LLM para detectar errores de reintento en sistemas de software

Bogdan Alexandru Stoica , Utsav Sethi , Yiming Su , Cyrus Zhou , Shan Lu , Jonathan Mace , Madan Musuvathi , Suman Nath

Un flujo de trabajo que reutiliza pruebas unitarias existentes para exponer errores relacionados con los reintentos en el software del sistema.

El comando de re -ejecución que se utiliza cuando falla una tarea se emplea habitualmente para crear sistemas de software resistentes, pero implementarlo y probarlo en sistemas modernos es todo un desafío. Basándose en problemas de reintento del mundo real , los autores presentan un conjunto de técnicas estáticas y dinámicas para detectar problemas de reintento . Descubrieron que la naturaleza ad hoc de la implementación de reintentos complica el análisis tradicional de programas, pero que los modelos de lenguaje grandes (LLM) pueden abordar estos problemas de manera eficaz. La investigación también demuestra que la reutilización de pruebas unitarias, combinada con la inyección de fallas, puede revelar varios problemas de reintento .


Escalado de la computación de aprendizaje profundo mediante el procesador de inteligencia conectada entre núcleos con T10

Yiqi Liu, Yuqi Xue, Yu Cheng, Lingxiao Ma , Ziming Miao , Jilong Xue, Jian Huang

Un ejemplo que asigna un operador MatMul a dos núcleos con el estilo de ejecución de cálculo por turnos. Tanto (b) como (c) son planes de ejecución de cálculo por turnos válidos, pero con diferentes compensaciones entre el uso de memoria y la sobrecarga de comunicación.

A pesar de los avances en chips de IA que permiten un acceso a la memoria entre núcleos con gran ancho de banda y baja latencia, los compiladores de aprendizaje profundo carecen de compatibilidad con conexiones escalables entre núcleos, lo que limita su potencial. Para abordar este problema, los autores presentan T10, un compilador de aprendizaje profundo de extremo a extremo que aprovecha la comunicación entre núcleos y la memoria distribuida en el chip. T10 presenta una abstracción tensorial distribuida, rTensor, y mapea el cálculo y la comunicación de los operadores tensoriales con un patrón de desplazamiento computacional generalizado a los núcleos. T10 optimiza el consumo de memoria en el chip y la sobrecarga de comunicación entre núcleos, seleccionando el mejor plan de ejecución.


SilvanForge: un compilador redirigido y guiado por programación para la inferencia de árboles de decisión

Ashwin Prasad , Sampath Rajendra , Kaushik Rajan , R Govindarajan, Uday Bondhugula

La figura ofrece una descripción general de la compilación guiada por programación con SilvanForge. La compilación se realiza a través de múltiples representaciones intermedias (IR), con optimizaciones en cada nivel y transiciones de un nivel al siguiente guiadas por una programación.

SilvanForge es un compilador redirigido guiado por programación para modelos basados ​​en árboles de decisión que explora varias opciones de optimización y genera automáticamente rutinas de inferencia de alto rendimiento para CPU y GPU. Consta de dos componentes principales: un lenguaje de programación para explorar de manera eficiente el espacio de optimización y un compilador redirigido que genera código para cualquier programación especificada. Al utilizar diferentes diseños de datos, estructuras de bucle y estrategias de almacenamiento en caché, SilvanForge logra un rendimiento portátil en múltiples destinos de hardware.


Descubrimiento del paralelismo de datos anidados y la reutilización de datos en la computación DNN con FractalTensor

Siran Liu, Chengxiang Qi, Ying Cao , Chao Yang, Weifang Hu, Xuanhua Shi, Fan Yang , Mao Yang

FractalTensor mejora la programación DAG para DNN con un ADT basado en listas, lo que permite que ideas algorítmicas DNN innovadoras se expresen de forma natural, que el compilador analice su paralelismo y, posteriormente, se traduzcan al procesamiento de mosaicos.

Las redes neuronales profundas (DNN) suelen utilizar operadores tensoriales altamente optimizados para acelerar el cálculo, pero estos operadores suelen definirse empíricamente, lo que limita el análisis y la optimización entre operadores. FractalTensor aborda este problema introduciendo un tipo de datos abstractos (ADT) basado en listas anidadas, donde cada elemento es un tensor con una forma estática u otro FractalTensor. Las DNN se definen entonces utilizando operadores de cálculo de orden superior como map/reduce/scan y operadores de acceso a datos como window/stride, exponiendo explícitamente el paralelismo de datos anidados y patrones de acceso de grano fino. Este enfoque permite el análisis y la optimización de todo el programa. Este documento solo estará disponible en las actas de SOSP 2024.


Descubriendo controles semánticos para programas de infraestructura en la nube como código

Yiming Qiu, Patrick Tser Jern Kon, Ryan Beckett y Ang Chen

El flujo de trabajo general de Zodiac. Comienza con la ingesta de repositorios de IaC extraídos de fuentes en línea. Basándose en un conjunto seleccionado de plantillas de comprobación que utilizan una base de conocimiento semántico (KB) y un lenguaje de especificación, genera un conjunto de comprobaciones hipotéticas. A continuación, realiza un filtrado estadístico y una interpolación para reducir los falsos positivos y completar los detalles faltantes con la ayuda de LLM. Las comprobaciones hipotéticas se introducen en la fase de validación. Para cada una de esas comprobaciones, Zodiac identifica las instancias que cumplen los requisitos y que podrían utilizarse como casos de prueba positivos y las modifica para obtener los casos de prueba negativos correspondientes. Una comprobación se valida si el caso de prueba positivo se implementa con éxito, pero su contraparte negativa no. Para resolver aún más los conflictos entre las distintas comprobaciones, Zodiac planifica el orden de generación e implementación de los casos de prueba negativos a través de un programador de validación.

Esta investigación presenta Zodiac, una herramienta que utiliza minería guiada por semántica y canales de validación basados ​​en la implementación para descubrir automáticamente las comprobaciones semánticas de IaC en la nube. Cuando se aplicó a los recursos de Microsoft Azure, Zodiac identificó más de 400 comprobaciones semánticas que causarían fallas en la implementación si se violaran, lo que demuestra su capacidad para detectar requisitos de la nube que son difíciles de encontrar para las herramientas de IaC de última generación.


Documento y tutorial

Verus: una base práctica para la verificación de sistemas

Premio al artefacto distinguido
Chris Hawblitzel , Jay Lorch

Diagrama general de Verus. Verus ofrece potentes técnicas de razonamiento automatizadas y semiautomatizadas que se aplican a toda la pila del sistema, así como técnicas de razonamiento adaptadas a niveles de pila específicos.

Este trabajo presenta una versión actualizada de Verus, una herramienta que acelera y simplifica la verificación formal del software del sistema. Se basa en avances anteriores para una verificación más rápida y rentable de propiedades complejas en sistemas realistas y ahora verifica el código hasta 61 veces más rápido que los métodos existentes. Se ha evaluado en varios sistemas que abarcan 6100 líneas de código y 31 000 líneas de prueba. Verus está listo para una adopción más amplia por parte de los desarrolladores que usan Rust y desean crear sistemas más robustos. Microsoft Blog. Traducido al español

Artículos relacionados

Scroll al inicio