Elmord's Magic Valley

Software, lingüística, mitologia nórdica e rock'n'roll

My very brief affair with Btrfs

2014-09-14 01:38 -0300. Tags: comp, unix, mundane, ramble

Meia dúzia de dias atrás eu migrei meu / para Btrfs. Hoje eu reformatei a partição como ext4 e recuperei meu backup do / da semana passada.

O causo foi assim. Para usar o Btrfs, eu atualizei meu kernel para o 3.16, já que diversas melhorias foram realizadas no suporte a Btrfs nessa versão. Porém, o driver da minha placa de rede wireless (o broadcom-sta) andava não se comportando muito bem, o iwconfig hoje resolveu não listar nenhuma rede, e eu resolvi bootar com o meu kernel 3.14 anterior para ver se a situação melhorava. (Na verdade, com a atualização do kernel 3.2 para 3.14, que eu fiz para poder usar o Btrfs, eu tive que substituir o broadcom-sta da stable pelo da testing, e desde então ele já andava com uns comportamentos desagradáveis (tais como emitir um trace sempre que a wi-fi era iniciada), mas aparentemente a wi-fi estava funcionando corretamente mesmo assim.) Até aí, tudo transcorreu normalmente. Kernel 3.14 bootado, wi-fi funcionando, todos comemora.

Eis que eu fui abrir o aptitude (já não lembro mais por que motivo), e o módulo do Btrfs capota, emitindo algum erro sobre quotas/qgroups. Reiniciei a máquina com o kernel 3.14, fui abrir o aptitude de novo, mesmo erro. Agora não lembro mais a seqüência exata das ações, mas em algum momento eu desativei o suporte a quotas (btrfs quota disable /), abri o aptitude de novo, e dessa vez ele abriu. Porém, turns out que, no piripaque do filesystem, meu /var/lib/dpkg/status virou um arquivo vazio, e o aptitude abriu me mostrando nenhum pacote instalado e me oferecendo para baixar 3GB de pacotes (i.e., todos os pacotes que eu tinha na máquina). Nesse momento eu me disse "well, fuck", reformatei o / como ext4 e recuperei o backup que eu tinha feito quando fui migrar para Btrfs (que por sorte eu ainda não tinha apagado).

Moral da história: Talvez se eu tivesse me mantido usando o kernel 3.16 eu não tivesse tido esse problema. Porém, depois dessa experiência, e dado que na atual conjuntura eu deveria estar me preocupando com o mestrado e não com a saúde do meu filesystem, eu prefiro esperar mais uns meses para ver se o Btrfs fica mais estável e experimentá-lo de novo. Enquanto isso, eu voltei para o kernel 3.2 da stable, que pode não ser new and shiny, mas é sólido como uma rocha, forte como um touro e pesado como uma porpeta.

3 comentários

Partição de sistema Btrfs no Debian

2014-09-12 03:03 -0300. Tags: comp, unix, mundane

Btrfs é um sistema de arquivos relativamente "recente" (o desenvolvimento começou em 2008) com um bocado de features interessantes. Neste post, falarei uma porção de coisas sobre como usar uma partição Btrfs como sistema de arquivos raiz no Debian. O Btrfs ainda é considerado experimental (embora seja bastante estável em kernels recentes), e eu não confiaria meus arquivos pessoais a ele no momento (meu /home é uma partição ext4), mas como sistema de arquivos raiz de uma máquina de uso pessoal (que se eu perder é só reinstalar), acredito que os benefícios compensam os riscos.

[Update: Aparentemente ele não é tão estável assim.]

E que benefícios são esses?

A principal razão pela qual eu migrei meu / para Btrfs foi para usar sua feature de snapshots, que permite criar uma "duplicata" do estado do sistema de arquivos em um dado momento. A criação de um snapshot não duplica os arquivos; ao invés disso, os arquivos são compartilhados entre as duas "versões" do sistema de arquivos, e só são copiados à medida em que são modificados, o que torna a criação do snapshot praticamente instantânea e não consome espaço desnecessariamente. Com isso você pode, por exemplo, tirar um snapshot do /, atualizar/bagunçar o sistema e, se alguma coisa der errado, voltar ao estado anterior são e salvo.

Requisitos mínimos

Kernel 3.14 ou superior. O suporte a Btrfs do kernel atual (3.2) do Debian stable é bastante precário (eu consegui derrubar ele com um for ((i=0; ; i++)); do mkdir $i; done em um filesystem recém criado). As opções são:

btrfs-tools 3.14 ou superior. Disponível tanto no repositório da backports quanto no da unstable.

Adaptando o initramfs

Para poder bootar a partir de um raiz Btrfs, você precisará adicionar suporte ao filesystem ao seu initramfs. Para isso, adicione as seguintes linhas ao /etc/initramfs-tools/modules:

crc32c
btrfs

e execute update-initramfs -u -k all.

A linha crc32c é particularmente relevante: Geralmente, o update-initramfs é esperto o suficiente para incluir junto com um módulo todas as suas dependências no initramfs. Porém, por um bug no módulo btrfs, ele não indica explicitamente sua dependência pelo módulo crc32c. Se o módulo crc32c não for incluído manualmente na lista, a carga do módulo btrfs falhará no boot, com uma mensagem do tipo can't load module btrfs (kernel/fs/btrfs/btrfs.ko): unknown symbol in module, or unknown parameter. (Isso me tomou uma boa hora de sofrimento.)

Migrando para Btrfs

Para transformar seu raiz em Btrfs, você precisará bootar com um outro sistema e seguir uma de duas rotas:

Antes de reiniciar

Antes de rebootar o sistema no filesystem recém criado, lembre-se de altarar o etc/fstab do sistema. Você poderá ter que trocar:

Se o seu /boot fica dentro na mesma partição que o raiz, você pode ter que fazer alguma mudança no seu gerenciador de boot para garantir que ele consiga ler o Btrfs. O GRUB 2 aparentemente consegue ler Btrfs sem problemas. (Eu ainda uso o bom e velho GRUB 0.97, mas meu /boot é uma partição ext2 separada.)

Subvolumes e snapshots

O Btrfs organiza o filesystem em subvolumes. Inicialmente, o filesystem contém apenas um "subvolume raiz", mas outros subvolumes podem ser criados com o comando btrfs subvolume create /caminho/novo-nome, onde /caminho é um diretório dentro do filesystem de interesse. btrfs subvolume list /caminho lista todos os subvolumes (e respectivos IDs) contidos em um filesystem.

O comando btrfs subvolume snapshot /caminho-subvol-origem /caminho-subvol-destino duplica um subvolume, i.e., cria um "snapshot". Depois da duplicação, os dois subvolumes são independentes: alterações em um não se refletem no outro.

Um filesystem Btrfs possui um subvolume padrão, i.e., o subvolume que é usado como raiz do filesystem se nenhum outro for especificado. Inicialmente, o "subvolume raiz" é o padrão, mas você pode usar o comando btrfs subvolume set-default ID /caminho (onde ID é o ID mostrado por btrfs subvolume list) para escolher outro. Com isso você pode setar o subvolume padrão para um snapshot com um estado anterior do sistema, por exemplo, reiniciar a máquina, e magicamente seu sistema volta a ser o que era no momento do snapshot.

Você pode montar um subvolume diferente do padrão passando a opção -o subvolid=ID para o comando mount. -o subvolid=0 monta o subvolume raiz original. Você pode montar a mesma partição mais de uma vez.

Como eu mencionei antes, ao invés de copiar o backup do sistema diretamente para o raiz da nova partição, pode ser mais conveniente criar um subvolume primeiro, especialmente se você pretende usar a feature de snapshots com freqüência. Por exemplo, ao criar o filesystem:

# mount /dev/xxx /mnt/sistema
# cp -avx /mnt/sistema /algum/lugar/backup
# umount /mnt/sistema
# mkfs.btrfs -f /dev/xxx
# mount /dev/xxx /mnt/sistema
# btrfs subvolume create /mnt/sistema/current
# btrfs subvolume list /mnt/sistema
ID 264 gen 142 top level 5 path current
# btrfs subvolume set-default 264 /mnt/sistema
# cp -avx /algum/lugar/backup/* /mnt/sistema/current
# (realize as adaptações pré-boot adequadas)

Com o subvolume padrão setado, você pode reiniciar e bootar o sistema novo normalmente. Quando você quiser fazer um snapshot, basta montar o raiz original em algum lugar (e.g., /mnt/root) e fazer as operações de interesse:

# mount -o subvolid=0 /dev/xxx /mnt/root
# btrfs subvolume snapshot /mnt/root/current /mnt/root/snapshot-20120912
# umount /mnt/root

Feito isso, você pode bagunçar com seu sistema à vontade e, se quiser voltar atrás, pode executar:

btrfs subvolume set-default ID-do-snapshot

e reiniciar a partir do snapshot. Ou, se preferir não alterar o snapshot, você pode duplicá-lo primeiro e reiniciar pela cópia:

# mount -o subvolid=0 /dev/xxx /mnt/root
# btrfs subvolume snapshot /mnt/root/snapshot-20120912 /mnt/root/current2
# btrfs subvolume list /mnt/root
ID 264 gen 142 top level 5 path current
ID 266 gen 142 top level 5 path snapshot-20120912
ID 268 gen 142 top level 5 path current2
# btrfs subvolume set-default 268 /mnt/root
# reboot

Lembre-se de depois apagar o current antigo (com btrfs subvolume delete /mnt/root/current), caso não queira que ele fique ocupando espaço para sempre.

A vantagem de criar um subvolume primeiro antes de copiar o sistema é deixar o subvolume raiz original contendo apenas subvolumes, evitando misturar subvolumes e arquivos de sistema no mesmo nível. Isso permite manipular todos os subvolumes/snapshots da mesma maneira (qualquer versão do sistema pode ser apagada facilmente, por exemplo; com o sistema no raiz original isso não seria possível).

Observações sortidas

O utilitário btrfs permite abreviar comandos, desde que as abreviações não sejam ambíguas. Por exemplo, btrfs subvolume list / pode ser escrito como btrfs sub l /.

Espaço usado e livre em Btrfs são conceitos um tanto quanto curiosos, devido ao mecanismo de copy-on-write, suporte a compressão e outras peculiaridades do Btrfs. O comando btrfs filesystem df /caminho pode dar um resultado mais preciso do que o df -h.

Descobrir o espaço utilizado por cada subvolume é uma questão mais complicada (até porque subvolumes podem compartilhar dados). Se o mecanismo de quotas for habilitado no subvolume raiz original (com o comando btrfs quota enable /mnt/root), é possível usar o comando btrfs qgroup show /, que lista a quantidade de dados apontada por cada subvolume e a quantidade de dados não compartilhada com nenhum outro subvolume (e que portanto seria liberada se o subvolume fosse apagado). Para mais informações, dê uma olhada neste artigo.

É possível criar um snapshot somente-leitura passando a opção -r para o comando btrfs subvolume snapshot. A vantagem é que é mais difícil de destruir um backup do sistema assim. A desvantagem é que não é mais possível bootar pelo snapshot como se fosse um sistema comum.

2 comentários

O que são capabilities e o que elas têm de tão mágico

2014-04-19 08:39 -0300. Tags: comp, prog, unix, security

Eu já falei de capabilities por aqui algumas vezes antes. Neste post tentarei explicar o que elas são e por que eu acho que elas são a panacéia universal (ok, não, mas por que eu acho que elas são um avanço em comparação com as permissões convencionais do Unix).

(Antes de mais nada, gostaria de ressaltar que as capabilities a que eu me refiro aqui não têm nada que ver com o que o Linux chama de capabilities, que são basicamente uma maneira de separar o tradicional balaio de poderes do root em unidades que podem ser atribuídas individualmente a processos (e.g., com isso é possível dar a um processo o poder de alterar o relógio do sistema sem conceder todos os outros poderes de root junto).)

Ok, que diabos são capabilities?

Uma capability é um objeto ou "token" que representa a habilidade de um processo de acessar um certo recurso, tal como um arquivo ou uma conexão de rede. Capabilities possuem três propriedades importantes:

Turns out que file descriptors no Unix possuem essas três propriedades. Ao abrir um arquivo no Unix, o processo recebe um número inteiro que é um índice na tabela de file descriptors do processo, que é acessível apenas pelo kernel. File descriptors abertos podem ser passados adiante para os filhos de um processo ou transferidos via sockets. Uma vez aberto o arquivo, as credenciais do processo são irrelevantes para o seu acesso: um processo pode, por exemplo, começar executando como root, abrir um recurso privilegiado (e.g., ouvir em uma porta menor que 1024), e depois trocar de credenciais para um usuário menos poderoso sem perder o acesso ao recurso privilegiado, pois a posse do file descriptor da conexão é suficiente para garantir-lhe acesso ao recurso. (Um file descriptor não é uma capability pura porque conserva outros dados além dos necessários ao acesso do recurso, tais como a posição do cursor no arquivo, o que dificulta seu uso compartilhado por outros processos depois de transmitido, mas em essência trata-se de uma capability.)

A mágica de um modelo de segurança baseado em capabilities, entretanto, é que todo acesso a recursos é feito por meio de capabilities, e um processo tem acesso apenas aos recursos representados pelas capabilities que lhe são entregues. No Unix, por outro lado, um processo recebe acesso implícito e mais ou menos inevitável a diversos recursos, tais como o filesystem e a habilidade de criar conexões de rede. É possível cercar o acesso a esses recursos, e.g., usando chroot para entregar um filesystem alternativo ao processo (mas não é possível não entregar filesystem nenhum ao processo) ou regras de firewall para bloquear o acesso do processo à rede (geralmente indiretamente, e.g., rodando o processo com outro usuário e bloqueando o usuário no iptables), mas há uma série de dificuldades e inconvenientes envolvidos:

A raiz do problema é que o modelo de segurança do Unix foi criado no contexto dos sistemas multi-usuário dos anos 1970, em que a preocupação primária era proteger os usuários uns dos outros e o sistema dos usuários. Hoje em dia as preocupações são outras: no caso de computadores pessoais, a maioria das máquinas roda com um único usuário, e queremos proteger o usuário de programas potencialmente mal-comportados (seja por conterem vulnerabilidades, seja por descuido do programador, seja porque o programa é intencionalmente malicioso) que o próprio usuário executa. No caso de servidores, queremos minimizar o potencial de desastre caso um serviço seja comprometido. Capabilities se encaixam melhor (acredito) com essas preocupações do que o modelo de segurança tradicional do Unix, pois permitem um controle maior de o que um processo é capaz de acessar. Ao invés de passarmos aos programas o acesso ao filesystem inteiro e os nomes de arquivos que queremos que o programa manipule, passamos capabilities aos arquivos de interesse, sem entregar o acesso a todo o resto do filesystem junto. Ao invés de chamar todos os programas com o poder de abrir conexões de rede, podemos passar esse poder apenas aos processos que realmente tenham que ter esse acesso.

E o browser?

A essas alturas você talvez esteja se perguntando: "Ok, meu filho, e como isso resolve o problema do browser? Eu não vou ter que entregar uma capability para acessar todos os meus arquivos para o caso de eu querer fazer upload de um deles? Hã? Hã?"

A solução é uma das coisas mais legais que se consegue fazer com capabilities. Lembre-se de que capabilities podem ser transmitidas entre processos. Isso significa que nós podemos ter um daemon (chamemo-lo fileopend) capaz de fornecer capabilities. Ao iniciarmos o browser, passamos a ele uma capability que é um canal de comunicação com o fileopend. Quando o usuário vai fazer upload de alguma coisa, ao invés de o browser abrir a janelinha de "Abrir arquivo", ele manda uma requisição de abertura de arquivo ao fileopend. O fileopend, então, mostra a janelinha de "Abrir arquivo" ao usuário. O usuário escolhe o arquivo, e então o fileopend o abre e envia a capability correspondente àquele arquivo específico para o browser. O browser, assim, só tem acesso a arquivos que o usuário tenha selecionado explicitamente na janela de "Abrir arquivo".

Genial, hã?

And we can do it right now!

Atualmente existe um projeto chamado Capsicum: practical capabilities for UNIX, que teve bastante progresso recentemente. Trata-se de uma implementação de capabilities no FreeBSD, que está sendo adaptada para o Linux. O projeto inclusive produziu uma versão do Chromium baseada em capabilities, usando uma idéia análoga à do fileopend (que eles chamam de "user angels") para abrir arquivos do usuário.

Mas teoricamente, seria possível implementar capabilities em user-space no Unix com uma pequena dose de faconice. No cenário mais simples, seria possível rodar cada processo com um usuário/grupo diferente (gerar um UID/GID para cada processo novo), em um chroot, com acesso à rede bloqueado no firewall, etc., apenas com um canal de comunicação com um daemon que intermediaria o acesso dos processos a todos os recursos, tais como arquivos, conexões de rede, etc. Esse daemon faria o papel do kernel em um sistema com suporte nativo a capabilities. O problema com essa abordagem é performance: todo acesso a recursos teria que passar pelo canal de comunicação entre os processos comuns e o daemon. Porém, uma vez que file descriptors podem ser transmitidos por sockets no Unix, seria possível usar o daemon apenas para criar e transmitir file descriptors (capabilities) para os processos. Uma vez de posse do file descriptor, o processo pode utilizar o recurso "nativamente". A perda de performance seria apenas na abertura de recursos, e talvez não fosse tão significativa. Anyway, graças ao Capsicum, estamos em vias de ter capabilities nativas no Linux (hopefully no kernel mainline) sem ter que apelar a gambiarras.

Unix is dead. Long live Unix.

Comentários

NSA operation ORCHESTRA, e alguns pensamentos sobre o estado atual da computação

2014-04-17 01:29 -0300. Tags: comp, prog, security, politics, ramble

No FOSDEM (Free and Open Source Developers' European Meeting) deste ano, Poul-Henning Kamp deu uma palestra muito interessante intitulada "NSA operation ORCHESTRA - Annual Status Report" (video, slides). A palestra, apresentada na forma de um report de um programa fictício da NSA, explora a idéia de o que a NSA poderia estar fazendo para coletar o máximo de informação com o menor custo possível. Possibilidades incluem:

Como diz nos slides da palestra, "A intenção foi fazer as pessoas rirem e pensarem, mas eu desafio qualquer um a provar que não é verdade."

A única coisa que não me agrada nessa palestra é a conclusão de que "this is a political problem" e de que é inútil fazer qualquer coisa do ponto de vista técnico. As ações da NSA são um problema político, mas: (1) isso não quer dizer que não possamos ou devamos buscar eliminar fontes de vulnerabilidades no software existente; (2) esse tipo de sabotagem poderia vir igualmente de uma organização privada com recursos suficientes, então o problema não é puramente político, no sentido de que mesmo nos livrando de governos maliciosos, o problema não desapareceu.

Ação política é importante, mas como desenvolvedores de software podemos tomar atitudes para mitigar o efeito de ações maliciosas sobre software. Para começar, podemos parar de usar ferramentas da idade da pedra, que facilitam a introdução (acidental ou deliberada) de falhas de segurança, como C/C++. O potencial de insegurança no C/C++ não é o mero descuido na hora de calcular os índices e o tamanho de um vetor (que por si só já é uma eterna fonte de vulnerabilidades). Em C/C++ existe o conceito de comportamento indefinido (undefined behavior), e cada versão nova do GCC/Clang/[insira seu compilador C/C++ favorito aqui] sai "melhor" em explorar comportamento indefinido para fins de otimização do que a anterior. A idéia básica é que se um programa realiza certas ações "proibidas" pelo standard da linguagem (e.g., acessar um elemento além do final de um vetor), o comportamento resultante do programa não é especificado pelo standard, então o compilador é livre para gerar um programa que faz qualquer coisa nesses casos. Por exemplo, suponha que você escreve algo como:

void foo(struct pessoa_t *pessoa) {
    int idade = pessoa->idade;

    if (pessoa == NULL)
        printf("Oops, pessoa inválida!\n");
    else
        printf("A idade da pessoa é %d.\n", idade);
}

pessoa é um ponteiro (potencialmente nulo) para uma estrutura de dados. Acessar o conteúdo apontado por um ponteiro nulo é um comportamento indefinido: um programa que faz isso é um programa incorreto. Logo, o compilador é livre para gerar código que não funciona no caso de o ponteiro ser nulo. Logo, o compilador pode assumir que pessoa não é um ponteiro nulo: se a hipótese do compilador for verdade, o programa estará correto, e se não for, tanto faz se o programa está correto. Mas se o ponteiro não é nulo (por hipótese), então o if na função é redundante (pois a condição é sempre falsa): o compilador pode descartar as linhas cor-de-burro-quando-foge do código resultante, como uma otimização. Foi exatamente uma otimização desse tipo que transformou um erro de programação no kernel do Linux em uma falha de segurança alguns anos atrás. Outras situações em que o compilador pode conspirar contra o programador incluem: remover verificações de overflow em operações aritméticas, pois signed overflow é indefinido em C/C++; reordenar acessos à memória, ignorando que outras threads podem depender do acesso em uma certa seqüência, se o programador não tomar o cuidado de forçar a ordem das operações; e inúmeras outras situações. Dado o grau de exploitação de comportamento indefinido nos compiladores C/C++ modernos, seja por avanços tecnológicos em análise estática, seja por influência da NSA/agentes soviéticos/illuminati/maçonaria, eu me sinto fortemente propenso a encarar o compilador C/C++ como um agente malicioso, e a idéia de minimizar o uso dessas linguagens parece cada vez mais appealing.

Outra medida técnica para reduzir a propensão dos sistemas computacionais a falhas de segurança é adotar modelos de segurança baseados em capabilities, em que o default é os processos não terem acesso a nada que não lhes seja explicitamente concedido, ao contrário dos modelos baseados em usuários, como o do Unix, em que é difícil ter certeza absoluta de quais são os poderes que um processo tem, e a grande maioria dos processos roda com mais permissões do que precisa (e.g., seu browser tem o poder de ler todos os seus arquivos pessoais, o tempo inteiro).

Falar é mais fácil do que fazer. Hoje em dia há uma falta de soluções práticas que nos permitam livrarmo-nos do C/C++ sem perder performance ou outras conveniências, ou sistemas baseados em capabilities que não sejam sistemas acadêmicos cuja adoção no mundo real é inviável. Estes são problemas nos quais eu pretendo trabalhar durante a minha existência neste mundo [aquela história de crowdfunding era só parcialmente brincadeira :)]; mais sobre isso em um post futuro, talvez. O ponto é que definitivamente há (muito) o que fazer do ponto de vista técnico para mitigar os efeitos de ações da NSA e outros agentes maliciosos.

5 comentários

Bounds checking elimination

2014-04-12 23:45 -0300. Tags: comp, prog, pldesign

Essa história de Heartbleed me lembrou de algumas coisas que eu tinha pensado meses atrás e não lembrava mais.

Para quem não sabe, o Heartbleed (concisamente explicado por este quadrinho do xkcd) é uma falha de segurança na OpenSSL (uma biblioteca que implementa os protocolos de comunicação segura SSL e TLS usada por basicamente todo o mundo) que permite a um atacante obter porções da memória do servidor potencialmente contendo dados como nomes de usuários, senhas, a chave privada do certificado servidor, etc.

Como 237% das falhas de segurança de software encontradas nos últimos 30 ou 40 anos, o Heartbleed é causado por um buffer overflow (tecnicamente "overread", pois trata-se de leitura e não escrita), e teria sido evitado se a OpenSSL tivesse sido escrita em uma linguagem que fizesse verificação de limites (bounds checking) antes de acessar uma posição de um vetor.

No fórum do xkcd, alguém escreveu:

Heartbleed is yet another example of why coding in C is a bad idea. A memcpy with an incorrect size caused all this because C compilers do no bounds checking. Heartbleed wouldn't have happened if OpenSSL had been written in, for example, Ada. Instead of an information leak that leaves no trace it would have been a denial of service at the worst.

Mais adiante na thread, alguém respondeu:

It's yet another example of why poorly written code is a bad idea. No amount of programming languages and frameworks is going to protect you from incompetent programmers.

A essa altura eu fechei a tab e fui ler outras coisas, porque se eu continuasse ali eu ia acabar respondendo com o equivalente virtual do soco na cabeça pra desentupir o cérebro. Isso é mais ou menos como ter um viaduto do qual diariamente caem carros há trinta anos, e se recusar a colocar um muro de proteção nas bordas, porque se alguém cai "a culpa é do motorista que foi incompetente".

But, but, but, bounds checking? Is it web-scale?

Se bounds checking é uma coisa tão mágica, por que não está todo o mundo usando linguagens que fazem bounds checking? A resposta, obviamente, é performance, a propriedade mais importante de qualquer software. Does it work? No, but it's fast! Ok, chega de comentários sarcásticos por ora. Eu já falei sobre a performance de bounds checking em um post anterior, onde fiz alguns benchmarks com código em C com e sem bounds checking (implementado manualmente com ifs no código testando se o índice está dentro dos limites do vetor e abortando a execução caso contrário). As conclusões no final foram que:

Do segundo item depreende-se que um acesso bounds-checked a um vetor é cerca de 25% mais lento do que um acesso direto. Assumindo que a maioria dos programas não consiste primariamente de acessos a vetores, esses 25% talvez não fizessem tanta diferença, e o benefício seria maior que o custo. (Disclaimer: talvez no caso geral o slowdown seja maior que 25%. Talvez eu faça mais uns benchmarks, só para não perder o costume, quando estiver mais disposto. Read on.)

O primeiro item é mais interessante: em algumas circunstâncias é possível provar que todos os acessos a um vetor estarão dentro dos limites, e nesses casos não é necessário fazer qualquer verificação em tempo de execução. Por exemplo (assumindo uma função hipotética length_of, que retorna o comprimento de um vetor), em um loop como:

for (i=0; i < length_of(vector); i++)
    printf("%d", vector[i]);

não é necessário verificar em tempo de execução se vector[i] está dentro dos limites do vetor, pois é possível ao compilador provar em tempo de compilação que i só adquire valores que são índices válidos do vetor. Para casos simples como esse, o gcc e outros compiladores já são capazes de fazer esse tipo de análise estática, como visto no post linkado; não se trata de uma tecnologia mítica e utópica. Os problemas começam a surgir quando temos coisas como:

int get(int vector[], int i) {
    return vector[i];
}

void foo() {
    ...
    for (i=0; i < length_of(vector); i++)
        printf("%d", get(vector, i));
}

pois a função get não sabe que será chamada com um índice válido. Se o compilador fizer inlining de get no corpo de foo, ele será capaz de eliminar o bounds checking, mas, no caso geral, não queremos sempre fazer inlining (get poderia ser uma função grande chamada em diversos pontos do código, por exemplo), e a função get (que poderia ter sido compilada separadamente) não pode assumir que quem a chamar lhe passará um índice válido.

Mas ela pode exigir. Imagine que pudéssemos escrever algo do tipo:

int get(int vector[n], int i)
    i>=0 && i<n;
{
    return vector[i];
}

i>=0 && i<n é parte da assinatura da função: além de ela exigir que o primeiro argumento seja um vetor de int e o segundo um int, ela também exige que a condição especificada seja satisfeita. Com isso: (1) a função pode assumir que a condição é verdadeira dentro do corpo, eliminando assim o bounds checking; e (2) o encargo de testar se a condição é verdadeira é passado para o chamador da função (foo, no nosso exemplo), onde há contexto suficiente para determinar se a condição é sempre verdadeira em tempo de compilação (por conta de ocorrer dentro do for, no nosso exemplo). Se esse for o caso, o bounds check pode ser eliminado do programa; caso contrário, o check é realizado em tempo de execução, garantindo que o acesso será seguro.

Mesmo em loops em que o range não está evidentemente nos limites do vetor é possível utilizar uma pequena dose de falcatrua para "amortizar" os checks. Por exemplo, em uma função como:

int sum(int vector[], int start, int end) {
    int i, total=0;
    for (i=start; i<=end; i++)
        total += vector[i];
    return sum;
}

não é possível eliminar completamente o checking, pois não sabemos de antemão se start e end é uma faixa válida de índices do vetor. Mas nem por isso precisamos fazer o checking dentro do loop. Ao invés disso, podemos transformar o código em:

int sum(int vector[], int start, int end) {
    int i, total=0;

    int length = length_of(vector);
    if (start < 0) out_of_bounds_exception();
    if (end >= length) out_of_bounds_exception();

    for (i=start; i<=end; i++)
        total += vector[i];
    return sum;
}

Se a execução passar dos ifs, então start e end são índices válidos no vetor, e não precisamos executar testes para cada acesso.

Só tem um pequeno problema na transformação acima: ela encerra o programa se end estiver além dos limites do vetor mesmo antes de vetor[end] ter sido acessado; basicamente uma exceção que ainda não aconteceu encerra o programa. Neste programa em particular isso não chega a ser um problema pois o comportamento observável do programa seria o mesmo, mas isso não é válido no caso geral. Por exemplo, poderia ser que eu soubesse de antemão que o vetor é encerrado por um valor 0, e escrevesse o código como:

int sum(int vector[], int start, int end) {
    int i, total=0;

    for (i=start; i<=end; i++) {
        if (vector[i] == 0) break;
        total += vector[i];
    }

    return sum;
}

Nesse caso, mesmo que eu passe um end inválido, pode ser que o meu programa termine com um resultado correto, desde que o vetor seja devidamente terminado com um 0. O compilador não tem dados suficientes para provar que o vetor terá o 0, entretanto, e portanto checks precisam ser inseridos. Ainda assim, é possível transformar o código em algo como:

int sum(int vector[], int start, int end) {
    int i, total=0;

    int length = length_of(vector);
    if (start < 0) out_of_bounds_exception();
    int bounded_end = min(end, length-1);

    for (i=start; i<=bounded_end; i++) {
        if (vector[i] == 0) break;
        total += vector[i];
    }

    if (end>bounded_end && i>bounded_end) out_of_bounds_exception();

    return sum;
}

que é menos trivial (e provavelmente pode ser escrito de maneira mais eficiente, mas menos clara para fins de exposição), mas preserva a semântica do programa (a prova é sugerida como exercício para o leitor).

Nem sempre os índices de vetores provêm de ranges seqüenciais. Um exemplo em que isso não ocorre é em uma busca binária, em que, para eliminar os checks, o compilador precisaria conseguir provar que (min+max)/2 está entre min e max*.

Outra situação é quando criamos um vetor de lookup reverso r que mapeia os valores de um vetor v aos índices correspondentes, i.e., se v[1] = 42, então r[42] = 1. Nesse caso, para eliminar os checks, o compilador precisa ter informação suficiente para saber que os valores de v são sempre índices válidos em r. O que pode ser viável se o tipo de v indicar qual é a faixa de valores válidos que o vetor pode conter. De qualquer forma, é interessante que esse tipo de assumption usualmente escondida sobre o comportamento do programa seja explicitamente expressível na linguagem, especialmente se tais declarações (1) não forem obrigatórias, e (2) forem usadas para melhorar performance. (Side-effect: as pessoas seriam incentivadas a documentarem melhor seus programas visando ganhar performance. Todos comemora.)

Caveats

Bounds checking é só um componente de memory-safety. Outro aspecto importante é garantir que os ponteiros/referências apontam de fato para objetos válidos em memória, e não para áreas que já foram desalocadas (ou pior, realocadas para outros objetos). A solução clássica para o problema é gerência automática de memória com garbage collection, mas há outras soluções possíveis.

O fato de que, com a introdução de pré-condições, os tipos das funções falam mais sobre o que a função faz, provavelmente implica que os tipos das funções mudam com mais freqüência quando uma função é alterada, efetivamente alterando sua interface, uma vez que cabe ao chamador da função garantir que as pré-condições são satisfeitas. Isso torna mais provável que uma alteração em uma biblioteca exija a recompilação de todo o mundo que depende dela. A solução que eu proponho é distribuir tudo como bytecode e (re)compilar para código nativo transparentemente as needed (o que tem inúmeras outras vantagens, tais como não fixar a ABI, permitir compilar o código com ou sem certs instruções (e.g., SSE) dependendo de sua disponibilidade no processador, permitir se aproveitar de mandingas brabas dependentes de uma versão da arquitetura (e.g., assumir que ponteiros têm efetivamente 48 bits e não 64 no amd64) sem se preocupar se daqui a 5 anos elas não vão mais funcionar, pois o ambiente pode simplesmente testar se uma assumption é válida e recompilar caso contrário, etc.). Uma solução alternativa é the C++ way: não fazer nada a respeito.

Conclusões

1. Bounds checking, galera. De uma vez por todas. Entre acidentes e talvez-nem-tão-acidentes, depois de 30 anos tá na hora de a gente aprender, não?

2. Bounds checking não necessariamente implica perda de performance, pois o compilador pode determinar que certos checks não são necessários em tempo de execução. Em uma linguagem sem bounds checking, o programador tem que ou inserir os checks manualmente anyway para garantir que não ocorrerá nenhum buffer overflow, ou concluir que o check não é necessário pois o índice está garantidamente dentro do vetor. No primeiro caso o check está lá anyway com ou sem bounds checking automático; com o check automático não há o risco de o programador esquecer de fazer o teste. No segundo caso o programador pode (idealmente) escrever explicitamente o raciocínio que permite concluir que o check é desnecessário, o que, além de menos error-prone (já que, se o compilador não for capaz de concluir que o raciocínio é válido, seja porque o raciocínio está errado ou porque o compilador não é suficientemente esperto, ele vai inserir o check dinâmico), é benéfico do ponto de vista de engenharia de software.

P.S.: Idéias similares às apresentadas neste post já foram inventadas e reinventadas mais de oito mil vezes sob os nomes de dependent types, design by contract, e sabe-se lá mais que outros (sinta-se à vontade para citar referências nos comentários). É por este motivo que, embora o tópico seja perfeitamente o tipo de coisa na qual eu gostaria de trabalhar, eu provavelmente não vou nem tentar empurrar o tema da minha dissertação de mestrado para esse caminho. Mais sobre isso em um post futuro, talvez.

_____

* Ou ser informado disso pelo programador, como um "axioma" sem prova. Nesse caso introduz-se uma fonte bastante perigosa de potenciais bugs, pois um axioma incorreto poderia levar a transformações de código incorretas em pontos arbitrários do programa. Uma solução semi-aceitável neste caso particular é ter uma função na biblioteca padrão da linguagem que calcula a média de dois números, acompanhada de um axioma sobre o resultado. O problema é que se a habilidade de declarar axiomas sem prova for introduzida na linguagem, é praticamente certo que alguém vá usá-la incorretamente e criar outro Heartbleed. Outra alternativa é introduzir um meio de o programador escrever a prova do axioma, que o compilador seria então capaz de verificar. Isto é nada mais, nada menos do que uma aplicação de proof-carrying code.

4 comentários

LaTeX vs. GPL, ou Vocês nunca entenderão o legalismus

2013-11-05 21:38 -0200. Tags: comp, copyright, ramble

Disclaimer: Este post, que começou muito bem-apessoado e com esperança de responder de maneira clara algumas questões, acabou virando um texto extremamente rambloso que não responde coisa nenhuma. You have been warned.

Estou escrevendo a monografia do meu TCC em LaTeX, usando um modelo do pacote iiufrgs, mantido pelo Grupo de Usuários TeX da UFRGS (UTUG). O iiufrgs é distribuído sob a GPL versão 2 ou superior. Software livre, que legal!, não? O problema é que a GPL exige que obras derivadas de uma obra sob a GPL também estejam sob a GPL. Surge, assim, uma questão que muito possivelmente não ocorreu à galera que resolveu distribuir o pacote sob a GPL: um documento produzido a partir de um pacote LaTeX sob a GPL é uma obra derivada do pacote?

No caso de a resposta ser sim, há algumas conseqüências práticas. As que me ocorrem no momento são:

Este post contém os meus palpites sobre o assunto.

Disclaimer[2]: Eu não sou advogado. Estes palpites baseiam-se no meu vago e duvidoso conhecimento das leis em questão e são oferecidos as-is sem qualquer garantia de qualquer tipo, incluindo mas não se limitando a etc etc ipsis literis hocus pocus etc. Use por sua conta e risco.

Derivados

O que conta como obra derivada? A GPLv2 diz (ênfase minha):

0. This License applies to any program or other work which contains a notice placed by the copyright holder saying it may be distributed under the terms of this General Public License. The "Program", below, refers to any such program or work, and a "work based on the Program" means either the Program or any derivative work under copyright law: that is to say, a work containing the Program or a portion of it, either verbatim or with modifications and/or translated into another language. (Hereinafter, translation is included without limitation in the term "modification".) Each licensee is addressed as "you".

"Translated into another language" supostamente se refere à tradução do programa para outras linguagens computacionais (e.g., compilação para linguagem de máquina).

Antes de mais nada, vale lembrar que os fontes em LaTeX são basicamente programas. Para fins deste post, "programa LaTeX" se refere a um arquivo escrito na linguagem LaTeX, e pdflatex se refere ao programa que lê programas LaTeX e produz PDFs. Há dois pontos a se considerar aqui:

  1. Usar um pacote GPL torna um programa LaTeX GPL?
  2. O PDF resultante de um programa GPL está coberto pela GPL?

A primeira questão é meio duvidosa. Distribuir seu programa LaTeX com comandos \usepackage que incluem pacotes GPL sem distribuir os pacotes junto definitivamente não torna seu programa GPL. Porém, no momento em que o programa é processado pelo pdflatex, pode-se considerar que ele foi combinado com o programa GPL, e o bolo alimentar resultante está sob a GPL. Essa discussão é similar à velha história de se um programa linkado com uma biblioteca GPL está sob a GPL ou não, que se reduz à questão de se um programa que usa uma biblioteca é uma obra derivada da biblioteca. A FSF acha que sim. Eu me limito a não achar nada.

A segunda questão contém várias subquestões. A primeira é se a geração de um PDF a partir de um programa LaTeX conta como uma obra derivada do programa. Isso depende em parte de o que exatamente o pdflatex faz com os arquivos. Eu vejo duas possíveis interpretações:

  1. O pdflatex lê o programa LaTeX e o compila para PDF. Nesse caso, o resultado é uma tradução do programa LaTeX para PDF, e portanto está coberto pela GPL;
  2. O pdflatex lê o programa LaTeX e executa suas instruções. Nesse caso, o resultado é meramente a saída do programa, e não uma tradução, e a saída de um programa GPL por si só não constitui uma obra derivada do programa, a menos que ela inclua trechos do programa ou modificações ou traduções de trechos. Isto é, o status da saída de um programa como obra derivada não depende do fato de ela ter sido produzida pelo programa, e sim por seu conteúdo.

E aqui eu também fico na dúvida, pois a coisa é um tanto quanto sutil. O que me impede de dizer que o que um compilador C faz é executar um programa em uma domain-specific language para geração de código de máquina? Nesse caso o binário seria só a saída da execução do programa, e portanto não seria uma obra derivada. "A menos que a saída contenha uma obra derivada", você me diz, apontando para o fato de que a tal saída poderia ser vista como uma "tradução" do programa C, e portanto uma obra derivada (por definição pelo parágrafo 0 da GPLv2), apesar de ter sido produzida por "execução", e não por "tradução". Mas o que conta como tradução? Se eu escrevo um programa que imprime a data atual, eu não posso considerar a saída como uma "tradução" do programa? Imagino que não, porque a saída não é "equivalente" ao programa: ela produz uma data fixa, e não a data atual. Mas e se o programa produzir uma saída fixa? Se P é o programa:

for (i=1; i<=5; i++) printf("%d ", i*i);

o programa

printf("1 4 9 16 25 ");

é uma tradução / obra derivada do programa P? Se a resposta for não, então um compilador super-otimizante corre o risco de produzir um executável que não é uma obra derivada do fonte. (Imagine a mesma situação com um código-fonte de milhares de linhas transformado beyond recognition por um compilador.) Mas se a resposta é sim, abre-se um precedente para considerar a saída de um programa cuja saída é sempre a mesma uma obra derivada do programa. Acontece que um programa LaTeX é exatamente um tal programa; ignorando coisas como geração da data atual na capa do documento, um programa LaTeX sempre produz um PDF "equivalente".

Me parece difícil nesse caso, entretanto, considerar o PDF diretamente como uma obra derivada do pacote, pois o pacote não gera sempre a mesma saída; o PDF não é "operacionalmente equivalente" ao pacote. Quem gera sempre a mesma saída é o seu programa, que por acaso usa o pacote. Porém, se o fato de "linkar" o programa com o pacote produz uma substância mista que é uma obra derivada do pacote, coberta pela GPL, o PDF seria a tradução dessa substância mista, e portanto uma obra derivada, e portanto coberta pela GPL.

Conclusão

A conclusão é que eu sinceramente não sei se o PDF produzido a partir de um programa LaTeX que usa um pacote GPL está coberto pela GPL, e que copyright é uma coisa não muito bem definida quando transposta para o mundo do software. O que eu sei é que todo esse transtorno poderia ter sido evitado se o pessoal do UTUG tivesse usado uma outra licença para o iiufrgs. Talvez simplesmente usar a LGPL ao invés da GPL resolva esse problema. Outra alternativa seria adicionar uma "linking exception" à nota de copyright dos arquivos do iiufrgs. Escrever os detalhes da exceção é sugerido como exercício para o leitor.

Comentários

Tudo o que você nunca quis saber sobre union types

2013-10-23 02:45 -0200. Tags: comp, prog, pldesign

Este post relata o que eu aprendi tentando misturar (ou combinar) uniões de tipos e polimorfismo paramétrico na mesma linguagem. Faz tempo que eu não escrevo um post de 20k que ninguém vai ler, então aproveito a oportunidade para documentar essas coisas todas antes que eu as esqueça. Este post está sujeito a alterações futuras (dada a impossibilidade técnica de produzir alterações passadas) caso eu lembre de mais algum detalhe.

Contexto

Para quem não sabe, meu tema de TCC é criar uma linguagem de programação funcional didática. A motivação por trás disso é reduzir os problemas encontrados pelos alunos da disciplina de Fundamentos de Algoritmos (da qual eu fui monitor por três anos) com a linguagem Scheme/Racket (especificamente, com as linguagens didáticas do How to Design Programs, doravante HtDP).

Um dos problemas com essas linguagens é a falta de um sistema de tipos estático. Como conseqüência, as funções e estruturas no código escrito na disciplina normalmente são acompanhadas de um pequeno comentário em um formato semi-padrão indicando os tipos dos parâmetros e retorno das funções, campos de estruturas, etc. O problema é que essa informação não é usada pela linguagem, o que significa que (1) ela não é lá muito útil; (2) conseqüentemente os alunos tendem a não escrevê-la; (3) não há qualquer validação sobre o formato dos comentários, o que impede os alunos de "testar" se eles estão corretos. Para resolver isso, a nova linguagem (que, por motivos de piada interna maior, chama-se Faz), é estaticamente tipada e permite (na verdade exige) declarar os tipos das funções e estruturas.

O problema é que diversos exercícios do HtDP utilizam tipos mistos. Tipos mistos são uma maneira semi-formal de descrever os tipos de funções e de dados freqüentemente utilizados em linguagens dinamicamente tipadas. Por exemplo, se uma função área aceita como argumentos quadrados e círculos, pode-se definir um tipo misto "forma" constituído por quadrados e círculos e dizer que a função recebe uma forma e produz um número. No HtDP, tipos mistos são "definidos" por meio de comentários no código.

A maioria das linguagens estaticamente tipadas não permite definir tipos mistos dessa maneira. Ao invés disso, a maioria das linguagens funcionais estaticamente tipadas permitem a declaração de uniões etiquetadas (tagged unions), ou sum types. Por exemplo, em Haskell, um tipo para formas poderia ser escrito como:

data Forma = Retangulo Float Float
           | Circulo Float

A declaração define o tipo (Forma) e os possíveis construtores de valores desse tipo (Retangulo, Circulo) e os tipos dos campos de cada construtor. Para criar um valor, escreve-se uma chamada ao construtor, tal como Retangulo 2 3 ou Circulo 4.

Uma união etiquetada é diferente de um tipo misto porque o tipo misto não exige uma etiqueta; é possível definir um tipo misto "número-ou-string" consistindo de números ou strings, por exemplo, sem definir novos construtores para o tipo novo. Embora a diferença possa parecer trivial, em muitos casos a ausência de tags é bastante conveniente. Por exemplo, alguns exercícios do HtDP definem uma "página Web" como uma lista contendo símbolos (palavras) e outras páginas Web (subpáginas). (I know, I know.) Um exemplo de "página Web" seria algo como:

(list 'Eis 'um 'exemplo 'de 'página 'web
      (list 'the 'quick 'brown 'fox 'had 'better 'things 'to 'do)
      (list 'whatever 'whatever 'bla))

Em Haskell, uma definição para esse tipo de dados ficaria algo como:

data Webpage = List [WebpageContent]
data WebpageContent = Word String | Sub Webpage

E o exemplo ficaria:

List [Word "Eis", Word "um", Word "exemplo", Word "de", Word "página", Word "web",
      Sub (List [Word "the", Word "quick", Word "brown", Word "fox", Word "had",
                Word "better", Word "things", Word "to", Word "do"]),
      Sub (List [Word "whatever", Word "whatever", Word "bla"])]

Que é "um pouco" menos conveniente. Poder-se-ia argumentar que a escolha de representação é tosca, mas de qualquer forma, uma vez que o meu objetivo era permitir transcrever os exercícios do HtDP para Faz com o mínimo de turbulência, eu queria encontrar alguma maneira de integrar os tipos mistos do HtDP na linguagem da maneira mais direta possível.

Então pensei eu: e que tal se adicionarmos uniões de tipos na linguagem? Uniões representam diretamente a idéia de tipos mistos. O usuário simplesmente diz:

tipo Coisas = Números U Strings

e agora 42 e "foo" pertencem ao tipo Coisas, sem necessidade de declarar tags. (Por baixo dos panos, a implementação guarda "tags" para saber os tipos dos valores, como em qualquer linguagem dinamicamente tipada, mas isso é um detalhe de implementação que não interessa ao usuário.) Simples, hã? Agora temos tipos mistos e tipagem estática. (By the way, a declaração acima é válida em Faz.)

Estranhamente, entretanto, aparentemente nenhuma linguagem estaticamente tipada usada por mais do que duas pessoas suporta uniões de tipos. Por que será?

Polimorfismo paramétrico

Haskell e companhia suportam uma coisa chamada de polimorfismo paramétrico (também conhecida por tipos genéricos no mundo C++/Java). Nessas linguagens é possível declarar coisas como "listas de α, para todo α", ao invés de declarar um tipo novo para cada tipo de lista que se deseja utilizar. Também é possível escrever funções de tipos genéricos. Por exemplo, uma função para incluir um elemento em uma lista nessas linguagens possuiria um tipo como (α, lista de α) → lista de α, i.e., uma função que recebe um argumento de um tipo α qualquer, uma lista de elementos do mesmo tipo α, e produz uma lista do mesmo tipo. Uma função que implementa o operador de composição de funções (f∘g), i.e, que recebe duas funções e produz uma terceira função que é equivalente a aplicar a segunda sobre o resultado da primeira, teria um tipo como (α→β, β→γ) → (α→γ), indicando que as funções podem ser de quaisquer tipos, mas o resultado da primeira tem que ser do mesmo tipo do argumento da segunda (β), e a função resultante recebe um argumento do mesmo tipo do da primeira (α) e produz um resultado do mesmo tipo do da segunda (γ).

A verificação/inferência de tipos nessas linguagens é feita usando o famoso Hindley-Milner type system e extensões do mesmo. Os detalhes podem ser um pouco sórdidos, mas, a menos que eu esteja viajando completamente, a idéia do Hindley-Milner é extremamente simples: ao checar uma expressão, gera-se uma lista de constraints (restrições) que devem ser satisfeitas para que a expressão esteja bem tipada. Por exemplo, se temos as seguintes funções (e respectivos tipos):

compose       : (α→β, β→γ) → (α→γ)
bool_to_int   : bool→int
int_to_string : int→string

então uma chamada como compose(bool_to_int, int_to_string) só é bem-tipada se:

α→β = bool→int
β→γ = int→string

Esta é a lista de constraints que devem ser satisfeitos. Do primeiro constraint, tem-se que:

α = bool
β = int

e do segundo,

β = int
γ = string

Como não há conflito entre os constraints, tem-se que a expressão é bem-tipada, e o tipo da chamada é α→γ = bool→string. Por outro lado, uma chamada como compose(bool_to_int, bool_to_int) produziria os constraints:

α→β = bool→int   =>  α = bool
                     β = int
β→γ = bool→int   =>  β = bool
                     γ = int

que não podem ser satisfeitos, e portanto a expressão é mal-tipada.

Enter subtyping

O Hindley-Milner foi feito para resolver constraints de igualdade. Em uma linguagem com relações de subtipagem (e.g., em que se pode declarar um tipo funcionário como subtipo de pessoa), aplicações de função não exigem mais que os tipos dos argumentos sejam iguais aos declarados para os parâmetros, mas sim que eles estejam contidos nos tipos dos parâmetros. Por exemplo, se pessoa tem os campos nome e idade, e funcionário tem os campos nome, idade e salário, então uma função como obtém_idade, do tipo pessoa → int, pode receber tanto pessoas quanto funcionários como argumentos.

E a presença de uniões de tipos basicamente introduz relações de subtipagem da maneira mais desenfreada possível: quaisquer dois tipos A e B possuem um supertipo comum, A U B. Isso significa que se temos uma função f do tipo (α, α) -> α, uma chamada como f(1, "foo") produz os constraints:

int ⊆ α
strings ⊆ α

que é satisfatível com α = int U string. Note que, na verdade, int U string é apenas um limite inferior para α: qualquer outro supertipo, como int U string U char, ou (top, o supertipo de todos os tipos), também serviria. Porém, intuitivamente int U string é o tipo mais "útil" inferível para a expressão, no sentido de que é o que mantém a informação mais precisa de que tipo de coisas se pode fazer com o resultado.

Nem sempre, entretanto, existe um único tipo "mais útil". A relação de subtipagem entre tipos funcionais possui uma propriedade curiosa: um tipo Sparam → Sreturn é subtipo de Tparam → Treturn, ou

Sparam → Sreturn ⊆ Tparam → Treturn

se

Tparam  ⊆ Sparam e
Sreturn ⊆ Treturn .

[Para entender essa inversão, você pode pensar assim: um tipo (S) é subtipo de outro (T) se S puder ser usado em qualquer lugar que T possa ser usado (e.g., funcionário é um tipo de pessoa porque um funcionário pode ser usado em qualquer lugar em que uma pessoa pode ser usada). Para que uma função (f) possa ser usada no lugar de outra (g), ela não pode exigir mais do argumento do que a outra, mas pode exigir menos (e.g., se g espera funcionários, então uma função que espere pessoas pode ser usada em seu lugar, pois funções que esperam pessoas também aceitam funcionários). Por outro lado, f tem que produzir um resultado tão bom ou melhor do que o da função que ela está substituindo (e.g., se g produzia pessoas, então f tem que produzir uma pessoa ou um funcionário, pois quem vai usar o resultado da função espera trabalhar com o resultado como se ele fosse uma pessoa).]

Agora imagine que temos uma função f do tipo (α→α) → (α→α), e uma função g do tipo int U string → int. A chamada f(g) produz o constraint:

int U string → int ⊆ α → α

de onde tem-se:

α ⊆ int U string
int ⊆ α

Tanto α = int quanto α = int U string são soluções válidas para os constraints, e nenhuma é evidentemente melhor que a outra.

Coisas como a chamada compose(bool_to_int, int_to_string) da seção anterior agora produzem constraints do tipo:

α ⊆ bool
int ⊆ β
β ⊆ int
string ⊆ γ

Destas, a única variável cujo tipo é fixado pelos constraints é β; as outras duas só possuem upper e lower bounds. Novamente, a solução "óbvia" ou "mais útil" seria α = bool, γ = string. Formalizar o "mais útil" no caso geral, entretanto, é um problema não-trivial e, como visto, nem sempre existe solução (o que fazer nesses casos é uma boa pergunta).

Variable identification

No Hindley-Milner, sempre que o constraint solver encontra um constraint da forma variável = whatever, ele substitui todas as ocorrências da variável por whatever no tipo e nos demais constraints, mesmo que whatever seja outra variável. Isso é válido porque os constraints são igualdades. No mundo da subtipagem, entretanto, igualar as variáveis nem sempre é a melhor solução. Por exemplo, considere as seguinte funções, escritas em um pseudocódigo funcional esquisito:

foo(f: α→β, g: α→γ, h: α→γ, k: β→γ) : Tripla(α→γ, α→γ, α→γ)
 = Tripla(compose(f, k), g, h)

jogo_do_pim(x: Int) : Int U String
 = if x mod 4 ≠ 0 then x
                  else "pim"

jogo_do_pi(x: Int) : Int U String U Char
 = if x == 4 then 'π'
   else if x mod 4 ≠ 0 then x
   else "pim"

id(x: ι) : ι
 = x

(Procurando por "jogo do pim" na Web encontrei um negócio interessante.) Agora, queremos tipar a chamada:

foo(jogo_do_pim, jogo_do_pi, id, id)

que produz os seguintes constraints, um para cada parâmetro/argumento (note que cada ocorrência de id usa variáveis de tipo separadas; caso contrário, todas as chamadas de id do programa teriam que ter o mesmo tipo):

Int → Int U String         ⊆  α → β
Int → Int U String U Char  ⊆  α → γ
ι  → ι                     ⊆  α → γ
ι′ → ι′                    ⊆  β → γ

Digerindo esses constraints, temos:

α            ⊆ Int
Int U String ⊆ β

α                    ⊆  Int
Int U String U Char  ⊆  γ

α ⊆ ι
ι ⊆ γ

β  ⊆  ι′
ι′ ⊆  γ

Se fôssemos igualar variáveis a la Hindley-Milner, teríamos, pelos dois últimos constraints, que α = γ e β = γ, e portanto α = β, mas não é possível resolver os constraints assim, pois α ⊆ Int e Int U String ⊆ β. Uma solução válida é:

α = Int
β = Int U String
γ = Int U String U Char

o que exemplifica que identificar/unificar as variáveis em constraints da forma α ⊆ β não é uma boa idéia na presença de union types (ou subtipagem em geral). Isso significa que podemos dar tchau para o Hindley-Milner. Só que agora temos um bocado de problemas. Por exemplo, suponha que temos os seguintes constraints:

α ⊆ Listas de β
β ⊆ Listas de α

Isto é um ciclo, que produziria um tipo infinito, o que em princípio é um erro. O Hindley-Milner facilmente detecta esta situação: ao encontrar o primeiro constraint, ele substitui todas as ocorrências de α por Listas de β, e o segundo constraint fica β ⊆ Listas de Listas de β. De forma geral, um ciclo sempre leva em algum ponto a um constraint em que a mesma variável aparece dos dois lados, o que é fácil de detectar. Sem igualamento de variáveis, essa abordagem não funciona.

Side note: para evitar a unificação, uma coisa que eu tinha pensado era, ao encontrar constraints do tipo α ⊆ Listas de β, substituir todas as ocorrências de α por Listas de α′, refletindo o fato de que se sabe que α é uma lista, mas não se sabe ainda de quê. O problema é que nesse caso o algoritmo entra em loop, pois:

α ⊆ Listas de β  => Listas de α′ ⊆ Listas de β            (expansão de α)
β ⊆ Listas de α     β ⊆ Listas de Listas de α′

                 => α′ ⊆ β                  (cortando o construtor comum)
                    β ⊆ Listas de Listas de α′

                 => α′ ⊆ Listas de β′
                    Listas de β′ ⊆ Listas de Listas de α′ (expansão de β)

                 => α′ ⊆ Listas de β′
                    β′ ⊆ Listas de α′       (cortando o construtor comum)

                    (... and so on ...)

Problema dos ciclos à parte, como devemos tipar uma expressão como compose(id, id)? A expressão produz os seguintes constraints:

α  ⊆  ι
ι  ⊆  β
β  ⊆  ι′
ι′ ⊆  γ

Qual é a solução? Unificar as variáveis? Mas em quais casos é correto unificar e em quais não é?

Instanciação ambígua de variáveis

A existência de uniões de tipos torna possível declarar coisas como:

f(x: Par(Int, α) U Par(α, String)) : α
 = if x.first ∈ Int then x.second
                    else x.first

Agora se chamarmos f(Par(5, "foo")), qual é a instanciação correta para tipo de x? α = Int ou α = String? Uma solução é detectar esse tipo de coisa e proibir que o mesmo tipo paramétrico apareça múltiplas vezes em uma união com um argumento que alterna entre concreto e abstrato. Da mesma forma, parâmetros de tipos como Int U α devem ser proibidos, pois a instanciação de α é ambígua quando o argumento é Int. E α U β também é ambíguo, pois para qualquer instanciação, a instanciação "flipada" (trocando os valores de α e β) também é válida. Supostamente essas restrições resolvem o problema, mas eu não estou quite sure quanto a isso.

O que eu fiz em Faz (sic)

Com o tempo limite para concluir o TCC se aproximando e a minha paciência/interesse no problema acabando, o que eu acabei fazendo foi um sério corte orçamentário na utilização de tipos paramétricos e uniões na linguagem. Para evitar o problema da unificação de variáveis, os casos em que ela é necessária são simplesmente proibidos: constraints da forma X ⊆ Y em que tanto X quanto Y contêm variáveis abstratas de tipos são rejeitados pelo typechecker. Isso significa que coisas como compose(id, id), em que tanto o parâmetro (α→β) quanto o argumento (ι→ι) são polimórficos, são rejeitadas. É tosco, mas pelo menos some com o problema. Além disso, uniões de tipos paramétricos também possuem algumas restrições (que eu ainda não defini direito, para ser sincero; quando eu terminar o TCC pode ser que eu edite esta seção).

Conclusão

Certa vez um sábio disse o seguinte:

Follow! But follow only if ye be man of valour! For the entrance to this cave is guarded by a creature, so foul, so cruel, that no man yet has fought with it and lived! Bones of full fifty men are strewn about its lair! So, brave knights, if you do doubt your courage or your strength come no further, for death awaits you all, with nasty, big, pointy teeth...

Acredito que ele estava falando de union types.

Comentários

Convertendo archives do LISTSERV para mbox

2013-09-04 01:45 -0300. Tags: comp, unix, prog, perl

Escrevi um pequeno script em Perl para converter um archive de mailing list do LISTSERV para o formato mbox, que pode ser importado em diversos clientes de e-mail. Possa ele ser-vos útil.

3 comentários

Zoom lento no MPlayer

2013-08-27 23:52 -0300. Tags: comp, unix, mundane

Esses dias fui assistir um filme com uma resolução maior do que a minha tela com o mplayer e meu Atom não estava dando conta de fazer o zoom out/scaling em tempo real.

Solução? O mplayer suporta uma opção -sws N, que permite escolher o algoritmo de software scaling a ser usado. Usando -sws 4, obtém-se um zoom de qualidade levemente pior, mas que consome menos processamento.

Outra opção útil é -autosync N, que controla a sincronia entre áudio e vídeo. A documentação do mplayer recomenda -autosync 30 para resolver problemas de sincronia com drivers de áudio problemáticos. No meu caso, -autosync 1 pareceu funcionar melhor. Não sei exatamente o que faz essa opção, sinceramente. Para mais informações, consulte a manpage do mplayer.

Quem me contou foi esse cara.

1 comentário

Determinando a posição do cursor em um arquivo com o lsof

2013-07-18 23:21 -0300. Tags: comp, unix, mundane

Às vezes executamos comandos do tipo:

cat imagem_grande_que_demora_para_copiar.img >/dev/sdb

e queremos saber o andamento do processo. Quando copiamos os dados de um disco para um arquivo podemos simplesmente olhar o tamanho do arquivo para ter uma idéia do andamento da operação, mas quando o destino é um disco isso não é possível.

É possível, entretanto, olhar a posição do cursor no arquivo. No Unix, todo arquivo aberto tem associado a si um cursor, i.e., a posição a partir da qual operações de leitura e escrita operam por padrão; cada leitura ou escrita no arquivo avança a posição do cursor.

Podemos utilizar um programinha chamado lsof (list open files, pacote lsof no Debian/Ubuntu) para visualizar diversas informações sobre arquivos abertos, dentre elas a posição do cursor. Por padrão, o lsof mostra uma coluna que contém ou a posição do cursor ou o tamanho do arquivo, dependendo do tipo de arquivo; a opção -o (offset) força o lsof a mostrar sempre o cursor. Além disso, por padrão o lsof mostra a posição em hexadecimal se ela ocupar mais de 8 dígitos decimais; a opção -o 0 desabilita esse comportamento. As duas opções podem ser combinadas como -oo0.

Por padrão, todos os arquivos abertos são listados. É possível especificar os nomes dos arquivos a serem listados, ou os nomes (-c nome) ou PIDs (-p pid) dos processos cujos arquivos abertos se deseja ver. Por exemplo:

# cat /dev/sda5 >/dev/sda6 &
[1] 28252
# lsof -oo0 /dev/sda6
COMMAND   PID USER   FD   TYPE DEVICE      OFFSET NODE NAME
cat     28252 root    1w   BLK    8,6 0t254476288 1303 /dev/sda6

Para mais informações, consulte a manpage do lsof.

Appendix A: Do fato de que ninguém deveria usar dd para copiar discos sem uma boa razão

# ls -lah foo
-rw-r--r-- 1 root root 512M Jul 18 23:00 foo
# time cat foo >bar

real    0m21.304s
user    0m0.068s
sys     0m5.212s
# time dd if=foo of=bar
1048576+0 records in
1048576+0 records out
536870912 bytes (537 MB) copied, 39.397 s, 13.6 MB/s

real    0m39.621s
user    0m1.528s
sys     0m25.910s

O motivo para isso é que o dd sempre copia os arquivos usando um tamanho de bloco fixo (indicado pelo parâmetro bs=tamanho, 512 bytes por padrão), enquanto o cat usa um tamanho de bloco "ótimo", o que permite que ele faça a cópia com menos chamadas de sistema (o que se reflete no tempo de sys na saída do comando time). Alternativamente, você pode especificar um tamanho de bloco maior para o dd (e.g., bs=1M), mas isso não apresenta nenhuma vantagem sobre usar o cat, a menos que você queira especificar o tamanho do arquivo também (e.g., no clássico dd if=/dev/zero of=foo bs=1M count=512 (que no entanto também pode ser substituído por um head -c 512M /dev/zero >foo)).

1 comentário

Main menu

Posts recentes

Tags

comp (74) unix (29) life (28) prog (26) random (22) mundane (20) lang (19) about (18) mind (14) web (13) rant (11) img (10) privacy (8) ramble (8) bash (7) esperanto (7) home (5) conlang (5) pldesign (5) lisp (4) freedom (4) book (4) misc (4) copyright (4) worldly (3) politics (3) kbd (3) film (3) security (3) music (3) academia (3) network (2) poem (2) android (2) mestrado (2) wrong (2) cook (2) editor (2) c (2) php (2) physics (2) pointless (1) shell (1) perl (1) audio (1) kindle (1)

Elsewhere

Quod vide


Copyright © 2012-2014 Vítor Bujés Ubatuba De Araújo
O conteúdo deste site, a menos que de outra forma especificado, pode ser utilizado livremente, com ou sem alterações, desde que seja mencionado o autor, preferivelmente com a URL do documento original.

Powered by Blognir.