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
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
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
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
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
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
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
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
Contacto