Elmord's Magic Valley

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

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

Muito bom, Hélio

2014-03-27 17:31 -0300. Tags: random, img, life

[A very disruptive idea]

Isto, meus caros, me foi apresentado como uma máquina de converter petróleo em pão. Durante uma aula. Depois de uma noite de três horas de sono. It was a very disruptive idea.

1 comentário

Padrão novo

2014-03-10 17:55 -0300. Tags: random, img

[Foto de tomada padrão antigo "adaptada" para o padrão novo]

E não pensem que foi fácil; aquele terra ali é funcional... eu acho.

5 comentários

Esse tal de mestrado

2014-02-12 02:08 -0200. Tags: academia, mestrado

Eu pretendia quebrar os últimos três meses de ausência com um post sobre a vida, o universo e todas as coisas, mas esse post não está com cara de sair tão cedo. Ao invés disso, apresento-vos um post de utilidade pública sobre como funciona a inscrição e a matrícula no mestrado no Programa de Pós-Graduação em Computação (PPGC) do Instituto de Informática da UFRGS. Alguns aspectos do processo são um tanto quanto obscuros/mal-documentados, e eu mesmo estou descobrindo aos poucos como as coisas funcionam. Minha idéia inicial era esperar até eu ter "todas" as informações relevantes para escrever; porém, até lá eu provavelmente já vou ter esquecido de metade delas (e, more importantly, das dúvidas que eu tive no processo), então vou começar a escrever com o que eu sei. Correções e coisas que eu descobrir posteriormente serão adicionadas a este post ou publicadas em outros posts com a tag mestrado. (Sim, todas as outras tags do blog são em inglês, mas não estou nem aí. Tal é a minha maldade.)

DISCLAIMER: Este texto baseia-se na minha experiência ao ingressar no mestrado em 2014/1. As regras e procedimentos descritos podem mudar em anos subseqüentes. As competências redatoriais do autor são questionáveis. Use por sua conta e risco. Dito isso, espero que estas informações lhe possam ser úteis.

POSCOMP

O primeiro passo para o ingresso no mestrado é a realização do POSCOMP, uma espécie de vestibular da pós-graduação em computação usado por diversas universidades do país. O POSCOMP consiste de 70 questões objetivas (20 de Matemática, 30 de Fundamentos de Computação, e 20 de Tecnologias de Computação).

As inscrições para o POSCOMP ocorrem por volta de julho, e a prova é aplicada por volta de setembro. A matrícula para o mestrado abre depois da realização do POSCOMP. Cada instituição decide como vai usar o resultado do POSCOMP. No caso do PPGC/UFRGS, exige-se que o candidato ao mestrado tenha realizado o POSCOMP no ano da inscrição ou no ano anterior, e que tenha obtido uma pontuação superior à média nacional (que em 2013 foi 30,7). A pontuação do POSCOMP é um dos critérios utilizados na seleção dos candidatos. Além disso, as bolsas de mestrado são dadas aos candidatos com maior pontuação. (Em 2013, foram selecionados 61 candidatos, dos quais 30 receberam bolsa.)

Se você não tiver feito o POSCOMP e não quiser esperar até o ano seguinte para entrar, o que você pode fazer é se inscrever como Aluno Especial no PPGC e ir cursando algumas das cadeiras enquanto não faz o POSCOMP. Tendo feito o POSCOMP, você pode se inscrever para o mestrado e pedir reaproveitamento das cadeiras já cursadas. Alunos Especiais não recebem bolsa, todavia.

Provas anteriores

As provas anteriores e gabaritos estão disponíveis no site da SBC e do COPS/UEL (que tem sido responsável pela aplicação das provas nos últimos anos). As provas e gabaritos de 2012 e 2013 encontram-se exclusivamente no site da UEL. As provas de 2010 e 2011 encontram-se em ambos os sites. As provas de 2002 a 2009 encontram-se apenas no site da SBC.

As provas de 2011, 2012 e 2013 já vêm com as respostas marcadas em vermelho, o que atrapalha o estudo. A solução que eu encontrei foi converter as páginas dos PDF em imagens e extrair apenas o canal azul (que tem intensidade 100% no fundo branco da folha e 0% no resto; o verde também serviria), usando o ImageMagick (pacote imagemagick no Debian/Ubuntu):

for ((i=1; ; i++)); do
    convert -density 150 "blablabla.pdf[$i]" -colorspace RGB -channel B \
            -separate -quality 80 prova-%02d.jpg || break
done

(Teoricamente, dá para especificar um intervalo de páginas para o ImageMagick, mas, pelo menos na minha máquina, ele come quilos de memória e leva um horror de tempo quando eu faço isso.) As outras provas possuem uma versão sem respostas. (As de 2009 para trás só possuem a versão sem resposta, com o gabarito separado.)

CUIDADO: há os gabaritos provisórios (divulgados logo depois das provas) e os definitivos (corrigidos depois de os alunos terem entrado com recurso). Todo ano cerca de duas a quatro questões acabam sendo corrigidas ou anuladas. Certifique-se de estar usando um gabarito definitivo quando estiver estudando.

Inscrição no PPGC

As inscrições para o mestrado no PPGC são feitas pelo site do PPGC. O edital contém um bocado de informação sobre a inscrição. Aqui listo alguns pontos que me parecem dignos de observação.

Ao inscrever-se, você pode escolher até três linhas de pesquisa de seu interesse, em ordem de prioridade. A cada linha estão associados um ou mais professores. Você pode escolher os orientadores de sua preferência, em ordem de prioridade, ou escolher "Qualquer orientador" na linha de pesquisa. Para descobrir o que faz cada professor, você pode consultar suas informações na página do PPGC, suas páginas pessoais (normalmente linkadas na página do PPGC), a pesquisa de currículos da plataforma Lattes, e seu mecanismo de busca favorito. Tendo se informado sobre um professor, você pode mandar e-mail para o mesmo para trocar uma idéia. Esse processo de catar professores em áreas de interesse e entrar em contato com os mesmos pode ser um tanto quanto demorado, então não deixe para a última hora.

O PPGC tem um bocado de professores (por volta de 60), então mesmo que sua área de interesse não se encaixe direito em nenhuma das linhas de pesquisa "oficiais" do PPGC, é bem provável que haja algum professor que trabalhe com algo próximo ao seu interesse. Assim, é uma boa idéia pesquisar e entrar em contato com os professores antes de concluir a inscrição.

Na inscrição, será exigido um comprovante de que você concluiu ou está em vias de concluir a graduação. No caso exclusivo de alunos da UFRGS, um comprovante de matrícula demonstrando que você está inscrito no trabalho de graduação é suficiente. Na inscrição, também é pedido um bocado de informações sobre o seu curso de graduação que em teoria podem ser obtidos na página do MEC. O formulário de inscrição é bastante ambíguo quanto às informações requisitadas, e eu não tenho muito o que lhe dizer a esse respeito. No caso exclusivo de alunos da UFRGS, você só precisa adicionar o curso de graduação, mas pode deixar os dados do MEC em branco. DISCLAIMER: esse procedimento não está descrito em lugar nenhum; eu descobri indo perguntar na secretaria do PPGC. Sendo assim, nada garante que o procedimento continuará válido nos anos seguintes, então é fortemente recomendado entrar em contato com o PPGC para perguntar como proceder.

A inscrição recomenda que você tenha um currículo na plataforma Lattes. Adicionar todas as informações no currículo é um processo que pode ser bastante tedioso/demorado, então é recomendável fazer isso o quanto antes (você pode fazer isso a qualquer momento, ao invés de esperar o período de inscrições, por exemplo).

Encerrado o período de inscrições, dá-se o processo seletivo. Se você escolheu mais de uma área ou mais de um orientador, em princípio a ordem em que você os escolheu será respeitada. (Os professores têm um número limite de alunos que podem orientar, então pode ser que sua primeira opção não seja atendida por falta de vagas.) Pode ocorrer de professores entrarem em contato com você para discutir outras possibilidades. Se você optar por um orientador diferente daquele que lhe seria atribuído segundo a ordem das suas escolhas, você terá que conversar com este para resolver a questão. NÃO deixe para fazer essa negociação de última hora, achando que tem até o final do processo seletivo para decidir. Embora isso não esteja escrito em lugar nenhum, o processo seletivo (mesmo antes da primeira chamada de divulgação de selecionados) é dividido em duas partes: inicialmente os selecionados são atribuídos aos orientadores de sua preferência, segundo suas escolhas na inscrição e eventuais negociações; depois dessa seleção, há um período de "repescagem", em que os candidatos que sobraram podem ser atribuídos a outros orientadores, mas em que as escolhas feitas na inscrição não têm mais a mesma prioridade. As negociações devem idealmente ser feitas antes desse segundo período.

[História da minha vida: escolhi um professor A na área X como primeira opção, e a área Y como segunda opção. Minha primeira escolha foi atendida. Porém, no dia 26/11, um professor B da área Y me mandou um e-mail perguntando se eu tinha interesse em trabalhar com ele e quando eu tinha disponibilidade para conversar. Como eu estava ocupado com o TCC e a data da primeira chamada que constava no calendário do PPGC era 13/12, deixei para conversar com o professor B apenas no dia 03/12. Turns out que a primeira etapa da seleção ocorreria no dia 05/12, i.e., eu só teria mais um ou dois dias para resolver o assunto. Eu tive sorte de conseguir conversar com os professores e outros alunos do PPGC nesse período e conseguir me decidir em tempo, mas foi uma situação bastante corrida e bastante estressante. Moral da história: não deixe para a última hora. The calendar is a lie.]

Se você for selecionado, alguns dias após a chamada você receberá um e-mail solicitando a confirmação de interesse no curso. Você deve seguir o procedimento descrito no e-mail; caso contrário, considera-se que você desistiu da vaga.

Matrícula

Uma vez selecionado, você deverá fazer sua primeira matrícula, que ocorre por volta de fevereiro. A matrícula é feita pelo Portal do Aluno da UFRGS. As instruções de acesso lhe serão enviadas por e-mail pelo PPGC.

O mestrado consiste de 24 créditos. O tempo recomendado de realização do mestrado é de dois anos; o PPGC recomenda que os 24 créditos sejam obtidos no primeiro ano, deixando o segundo apenas para a realização da dissertação de mestrado. A disciplina/atividade "CMP401 - Trabalho Individual I" é obrigatória e confere 2 créditos. A disciplina/atividade "CMP410 - Atividade Didática I" é obrigatória para os alunos bolsistas e confere 1 crédito.

Ao entrar no mestrado, você deve montar um Plano de Curso, que especifica que cadeiras você pretende fazer ao longo do curso e em que semestres pretende cursá-las. A maioria das disciplinas são oferecidas apenas no primeiro ou apenas no segundo semestre. A lista de disciplinas oferecidas pode ser encontrada no site do PPGC. O plano pode ser adaptado no futuro, no caso de haver alterações nas disciplinas disponibilizadas nos semestres futuros, ou no caso de as disciplinas que você escolheu conflitarem em horários, por exemplo.

A página da matrícula (que é comum a toda a UFRGS) é separada da página onde se submete o plano de curso (que é específica do PPGC, e é a mesma página onde você fez a inscrição para o mestrado). Na matrícula você seleciona apenas as cadeiras que pretende cursar no semestre corrente, enquanto no plano de curso você seleciona todas as cadeiras que pretende cursar no curso. Cabe a você fazer a matrícula consistente com o plano. Freqüentemente, a súmula do site do PPGC é menos detalhada do que a do site da matrícula. A vida tem dessas coisas.

Tanto a matrícula quanto o plano do curso devem ser aprovados pelo orientador para serem aceitos. Assim, convém falar com o mesmo antes de fazê-los.

Bolsa

A bolsa de mestrado atualmente é de R$ 1500 por mês. Ela é oferecida apenas aos alunos que cursarem o mestrado com dedicação exclusiva (i.e., não estiverem realizando outra atividade remunerada em paralelo). As bolsas, teoricamente em número limitado, são distribuídas pela ordem de colocação dos candidatos no POSCOMP. A partir de que mês a bolsa é paga e o processo burocrático para recebê-la são coisas que eu descreverei aqui assim que obtiver essas informações.

Miscelânea

Não existe entrevista na seleção para o mestrado. A entrevista existe para o doutorado (acho).

Você tem que escolher uma linha de pesquisa e um orientador na inscrição, mas não precisa ter um tema de mestrado definido já no começo.

Depois de inscrito no mestrado, você deve realizar um exame de proficiência (de leitura?) em língua estrangeira (a qual é necessariamente inglês), mas eu ainda não sei como isso funciona.

Se você acha que alguma outra informação deveria ser inclusa aqui, deixe um comentário.

1 comentário

Spam, spam, spam

2013-11-10 00:26 -0200. Tags: about

Em comemoração ao 150-ésimo post do blog, apresento-vos uma análise do comportamento dos spambots que me visitam tão assiduamente por aqui.

[Sir Spamalot]
Ilustração by Hélio encontrada em um caderno

Desde o dia 15/04/2012 até ontem (572 dias), os logs do blog registram 2051 tentativas de submissão de comentário. (Os logs têm um furo de cerca de duas semanas nesse período por um pequeno descuido com os arquivos.) Destas, 386 foram comentários bem-sucedidos (contendo a "resposta"). As outras 1665 são tentativas mal-sucedidas, das quais a grande maioria são spambots. (Algumas são pessoas que esqueceram de pôr a resposta ao submeter.) Isso dá uma média de 2.91 tentativas de spam por dia. Na prática, a quantidade de spam diário atualmente é maior que isso, pois a quantidade foi aumentando com o tempo:

# cat htlog-* | grep 'array ('  | grep -v "'cmmanswer' => 'XLII'"  |
  cut -d- -f1,2 | sort | uniq -c | sort -k2
      4 2012-04
      4 2012-05
     10 2012-06
      8 2012-07
      7 2012-08
     14 2012-09
    100 2012-10
     41 2012-11
     36 2012-12
     79 2013-01
     82 2013-02
     70 2013-03
     92 2013-04
     90 2013-05
    147 2013-06
    156 2013-07
    208 2013-08
    180 2013-09
    300 2013-10
     37 2013-11

2013-11 está menor do que o esperado porque estamos no começo do mês. Curiosamente, outubro de ambos os anos apresentam picos. Spam season?

Os "países" mais spamosos (baseado na saída do geoiplookup) são:

306     RU, Russian Federation
262     PL, Poland
216     UA, Ukraine
181     IP Address not found
157     US, United States
120     CA, Canada
99      CN, China
83      FR, France
81      LU, Luxembourg
52      A1, Anonymous Proxy
24      BR, Brazil
16      RO, Romania
15      NL, Netherlands
12      BE, Belgium

O conteúdo dos spams é que apresenta algumas surpresas. Por exemplo, o camarada 46.21.144.*, da Holanda, submeteu 14 comentários similares a esse:

Nome: 'lubgevvza'
Site: 'http://yngezlobxfcn.com/'
Resposta: 'Ac7NmB'
Texto: 'URFM5N <a href=\\"http://bpsgeffyfmzo.com/\\">bpsgeffyfmzo</a>, [url=http://gurqntepjlik.com/]gurqntepjlik[/url], [link=http://fdqlcjpcplfo.com/]fdqlcjpcplfo[/link], http://axymrrxyrgif.com/'

Os domínios mencionados não existem, e os acessos ocorrem em abril do ano passado e depois só em janeiro e fevereiro deste ano de novo.

Outra classe de spam são os comentários do tipo "whoa, que legal o teu texto, clique aqui":

Nome: 'strona główna'
Site: 'flazsdwtu@gmail.com'
Resposta: 'http://ths.pl/product-pol-5745-CERSANIT-Wanna-asymetryczna-CALABRIA-170-lewa-.html'
Texto: 'Throughout this great scheme of things you actually secure an A+ for hard work. Exactly where you lost everybody was first in your facts. You know, it is said, details make or break the argument.. And it could not be more correct here. Having said that, let me tell you just what did give good results. Your authoring is definitely extremely convincing and this is possibly the reason why I am taking the effort to opine. I do not make it a regular habit of doing that. 2nd, although I can certainly notice a leaps in logic you come up with, I am definitely not confident of just how you appear to unite your points which inturn make the final result. For right now I shall yield to your issue but wish in the future you actually link the dots much better. <a href=\\"http://ths.pl/product-pol-5745-CERSANIT-Wanna-asymetryczna-CALABRIA-170-lewa-.html\\" title=\\"strona główna\\">strona główna</a>'

(No post sobre o IPA.)

Ou:

Nome: 'discount homecoming dresses uk'
Site: 'uizckrptegw@gmail.com'
Resposta: 'http://eyeuser.com/blogs/viewstory/2127697'
Texto: 'Adult web Step into this I was suggested this web site by my cousin. I am not sure whether this post is written by him as nobody else know such detailed about my trouble. You’re wonderful! Thanks! your article about Adult web Step into this Best Regards Veronica Lawrence discount homecoming dresses uk http://eyeuser.com/blogs/viewstory/2127697'

(No post sobre prevérbios.)

Outros são pessoas se oferecendo para escrever por mim:

Nome: 'supra shoes'
Site: 'cttmmddww@gmail.com'
Resposta: 'http://www.suprashoes-skytop.com'
Texto: 'Please let me know if you’re looking for a article author for your blog. You have some really good articles and I think I would be a good asset. If you ever want to take some of the load off, I’d really like to write some material for your blog in exchange for a link back to mine. Please shoot me an e-mail if interested. Thank you!'

O mais legal de todos era um que continha uma conversa altamente filosófica sobre a Europa na Idade Moderna com links aleatórios no meio, mas não consegui mais encontrar.

Outra surpresa que eu tive agora é que das 1665 tentativas, 706 estão submetendo o formulário incorretamente, e não teriam sucesso mesmo que não houvesse qualquer mecanismo de antispam. O formulário para submissão de comentários do blog começa com:

<FORM ACTION='#cmmstatus' METHOD='POST'>

Aparentemente um bocado de bots descarta a query string (?entry=...) da URL do post ao submeter, enquanto o correto é submeter usando a mesma query string se nenhuma for especificada na ação (e o método não for GET; nunca testei o que acontece se o método é GET...). O post sobre o IPA parece ser particularmente atrativo a spambots, com 261 tentativas, seguido do post sobre múltiplos keymaps com o XKB e o sobre a performance de bounds checking.

Algumas das palavras mais freqüentes no texto dos spams, eliminando palavras funcionais (e.g., is, of, the, etc.):

    707 online
    547 asia
    537 shoes
    521 million
    429 seattle
    427 kings
    424 blog
    415 nba
    378 ranadive
    369 button
    312 sacramento
    311 nike
    276 buttons
    273 startup
    257 deal
    248 franchise
    244 claims

Um bocado dessas palavras (shoes, nba, ranadive, nike, kings) provêm de comentários gigantes com notícias sobre times de basquete com links perdidos para vendas de sapatos.

1 comentário

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

A personal appeal

2013-10-04 23:20 -0300. Tags: misc

[Creepy Jimmy Wales]

Alguns meses atrás eu tive este diálogo:

them: onde tu aprendeu tantas coisas?
me: na Wikipédia, a fonte de todo o conhecimento :P
them: achei que nas aulas de história
them: =P
me: pfff, aulas
me: a parte boa de estudar em colégio público é que eu tinha um horror de tempo livre pra ler a wikipédia :P
them: tb estudei em colegio publico
[...]
them: mas na minha época internet não era tão difundida
me: fora que quando eu tava no ensino fundamental eu não sabia inglês suficiente pra ler a wikipédia :P
me: na real eu meio que aprendi inglês lendo a wikipédia
me: cara
me: cara
me: ano que vem acho que eu vou fazer uma doação pra wikipédia :P
them: =D
them: se rendeu aos encantos deles?
me: não, cara
me: só me dei conta de que eles são mais responsáveis pela minha educação do que o colégio :P

Eu tenho usado a Wikipédia quase que diariamente nos últimos sete anos. Este ano a Wikipédia começou a aceitar doações por boleto bancário no Brasil, então resolvi fazer uma doação (de 20 pila) pela primeira vez. Doações podem ser feitas por aqui.

2 comentários

Main menu

Posts recentes

Tags

comp (72) unix (27) life (26) prog (26) random (22) mundane (18) about (18) lang (17) mind (13) web (13) img (10) rant (9) privacy (8) bash (7) esperanto (7) ramble (5) pldesign (5) conlang (5) misc (4) home (4) book (4) freedom (4) copyright (4) lisp (4) music (3) kbd (3) politics (3) film (3) security (3) poem (2) physics (2) worldly (2) editor (2) android (2) network (2) cook (2) c (2) academia (2) wrong (2) php (2) perl (1) pointless (1) mestrado (1) shell (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.