Resumo Técnico: Lógica de Separação para Detecção de Conflitos de Memória em Síntese de Alto Nível

Declaração do Problema

A Síntese de Alto Nível (HLS) acelera o desenvolvimento de hardware ao traduzir código C/C++ em designs de Nível de Transferência de Registrador (RTL), aproveitando o desenrolamento de loops (loop unrolling) e o particionamento de arrays para maximizar o paralelismo. No entanto, um gargalo crítico surge ao agendar acessos simultâneos à memória envolvendo aritmética não afim (ex: multiplicação, divisão ou módulo simbólicos).

Os frameworks de HLS tradicionais baseiam-se no modelo poliedral para análise de dependência. Esta abordagem geométrica exige que os limites dos loops e as funções de acesso a arrays sejam afins (combinações lineares de variáveis de loop). Quando confrontados com índices não afins, os solvers poliedrais sobre-aproximam sistematicamente as dependências para garantir a segurança. Isso força um recuo conservador: assumir que todas as instruções de memória dependem umas das outras, resultando em uma alocação de heap monolítica e na serialização de operações que poderiam, de outra forma, rodar em paralelo. Essa serialização artificial degrada o rendimento (throughput) e a eficiência do hardware. Além disso, as técnicas dinâmicas existentes frequentemente exigem verificações em tempo de execução ou controladores especializados, o que adiciona overhead.

Metodologia

O artigo propõe um framework de verificação espacial que opera diretamente na Representação Intermediária (IR) do LLVM para detectar conflitos de memória sem depender de restrições geométricas afins. A metodologia central integra a Lógica de Separação (SL) com a resolução de Satisfatibilidade de Teorias (SMT).

1. Modelagem Espacial no Nível de IR do LLVM

Ao contrário de abordagens anteriores que analisam Árvores de Sintaxe Abstrata (AST) de C/C++, este framework opera no IR do LLVM. Ele utiliza a instrução getelementptr (GEP), que o compilador usa para achatar mecanicamente índices de arrays multidimensionais em expressões aritméticas unidimensionais.

• Arquitetura de Estado Duplo: O framework modela o estado do sistema usando dois componentes distintos:
  • Armazenamento Monotônico ($s$): Mapeia registradores virtuais de Atribuição de Registro Simples Estática (SSA) imutáveis para valores. Devido ao SSA, os registradores nunca são sobrescritos, simplificando o rastreamento de estado.
  • Heap Espacial ($h$): Mapeia endereços físicos de memória (um subconjunto de valores) para dados, representando bancos de SRAM on-chip.
• Predicados de Banco Polimórficos: O framework define predicados espaciais bank(k, A, N) que afirmam a propriedade exclusiva do $k$-ésimo banco de memória para o array $A$ particionado em $N$ bancos. Esses predicados adaptam-se dinamicamente com base na estratégia de particionamento (Cíclica, em Bloco ou Completa) extraída dos metadados do LLVM.

2. A Condição de Desenrolamento Livre de Conflitos (CFU)

Para verificar se $U$ iterações de um loop desenrolado podem executar concorrentemente sem riscos estruturais, o framework formula a Condição de Desenrolamento Livre de Conflitos (CFU).

• Conjunção Separadora ($\ast$): O núcleo da verificação é a conjunção separadora iterada:
  $$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$$
  Isso afirma que os $U$ acessos simultâneos à memória devem possuir $U$ regiões de memória física estritamente disjuntas.
• Colapso Espacial: Um axioma fundamental da Lógica de Separação é que um recurso não pode ser possuído disjuntamente por si mesmo ($P \ast P \implies \bot$). Se duas iterações concorrentes visarem o mesmo banco físico $k$, a fórmula espacial tentará avaliar $bank(k) \ast bank(k)$, o que logicamente colapsa em uma contradição ($\bot$). Este colapso serve como a detecção matemática de um conflito de memória.

3. Tradução para SMT e Recuo (Fallback)

Para tornar a lógica espacial computável, o framework emprega uma função de tradução $T$ que reduz o requisito de disjunção espacial em uma matriz de desigualdades de pares sobre variáveis SSA.

• Condição de Verificação (VC): O requisito espacial é traduzido em uma fórmula de lógica de primeira ordem:
  $$\pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)$$
  onde $\pi$ é a condição de caminho e $k_i$ são os índices de banco simbólicos.
• Oráculo SMT: Um solver SMT (ex: Z3) tenta provar a VC.
  • Sat (Satisfatível): Os índices são comprovadamente distintos; o escalonamento paralelo prossegue.
  • Unsat/Unknown/Timeout: Se o solver não puder provar a disjunção (devido à aritmética inteira não linear indecidível), o framework aciona um recuo sequencial determinístico. Ele assume que existe um risco, serializando as operações via lógica de stall controlada por multiplexadores para garantir a segurança física.

Principais Contribuições

1. Modelo de Memória de Hardware Formal: O artigo estabelece um framework de memória estática sobre o IR do LLVM, abstraindo índices de arrays multidimensionais via instruções GEP e vinculando-os a predicados espaciais polimórficos que lidam com particionamento cíclico, em bloco e completo.
2. Condição de Desenrolamento Livre de Conflitos (CFU): Um requisito de execução espacial definitivo é formulado usando conjunção separadora iterada. Ele detecta riscos de bancos de memória através do colapso automático da lógica espacial ($cfu \implies \bot$) em vez de sobre-aproximação geométrica.
3. Tradução Automática para SMT e Recuo: Uma função de tradução matematicamente sólida reduz proposições espaciais a desigualdades de pares sobre registradores SSA imutáveis. Crucialmente, inclui um modelo de recuo sequencial conservador para garantir segurança absoluta quando a aritmética inteira não linear é indecidível.
4. Teorema de Correção (Soundness): O artigo prova que, se a Condição de Verificação algébrica for validada pelo solver SMT, o RTL sintetizado resultante é estruturalmente imune a colisões de banco de memória.

Resultados e Significância

O artigo afirma preencher a lacuna entre a teoria da lógica de separação formal e a síntese de hardware prática. Ao deslocar o ônus da verificação dos modelos poliedrais geométricos para a resolução algébrica de SMT sobre o IR do LLVM, o framework:

• Minimiza a Serialização Conservadora: Evita o recuo "seguro, mas lento" das ferramentas tradicionais ao encontrar índices não afins, desde que o solver SMT consiga resolver as restrições algébricas.
• Garante a Segurança Estrutural: Através do mecanismo de "Colapso Espacial" e do recuo conservador, o framework garante que nenhum hardware sintetizado sofrerá colisões estruturais de memória, mesmo na presença de aritmética indecidível.
• Ultrapassa as Limitações Afins: Resolve dependências complexas de mapeamento de banco sem exigir limites geométricos lineares ou gerar overhead adicional de máquina de estado em tempo de execução.

A significância reside em fornecer uma alternativa algébrica rigorosa ao modelo poliedral para o escalonamento de HLS, permitindo maior paralelismo em designs com padrões de acesso à memória não afins, mantendo as garantias absolutas de segurança exigidas pela geração de hardware. Os autores observam que o trabalho futuro envolverá a implementação disso como um pass customizado do LLVM e a exploração de permissões fracionárias para otimizar acessos simultâneos de leitura.