pikos_popl2020
1.0.0
Este é o artefato de software que acompanha o artigo "Computação determinística de ponto de fixação paralelo" de Sung Kook Kim, Arnaud J. Venet e Aditya V. Thakur.
"Computação determinística de ponto de fixação paralelo" pré -impressão: http://arxiv.org/abs/1909.05951.
@article{DBLP:conf/popl/KimVT20,
author = {Sung Kook Kim and
Arnaud J. Venet and
Aditya V. Thakur},
title = {Deterministic Parallel Fixpoint Computation},
journal = {{PACMPL}},
volume = {4},
number = {{POPL}},
pages = {14:1--14:33},
year = {2020},
note = {To appear},
url = {https://doi.org/10.1145/3371082},
doi = {10.1145/3371082},
}
@article{DBLP:journals/corr/abs-1909-05951,
author = {Sung Kook Kim and
Arnaud J. Venet and
Aditya V. Thakur},
title = {Deterministic Parallel Fixpoint Computation},
journal = {CoRR},
volume = {abs/1909.05951},
year = {2019},
url = {http://arxiv.org/abs/1909.05951},
archivePrefix = {arXiv},
eprint = {1909.05951},
}
Consiste principalmente em nossos Pikos paralelos de intérprete abstrato, 4330 benchmarks utilizados nos experimentos e scripts para reproduzir os resultados no artigo.
Pikos é baseado em um intérprete abstrato seqüencial, IKOS. Os arquivos alterados no IKOS para implementar PIKOS estão resumidos em CHANGES.md . Dado um programa como entrada, tanto os invariantes de IKOS quanto Pikos computam em cada ponto do programa e executam verificações neles. De fato, o PIKOS é implementado como uma opção de análise de IKOS, permitindo que ele calcule os invariantes em paralelo usando vários núcleos de CPU. Portanto, o PIKOS exige que as máquinas multi-core reproduzam os resultados. Requer pelo menos 16 núcleos para reproduzir todos os resultados. Ikos é escolhido como linha de base.
Depois de construir e instalar Pikos, pode -se executar Pikos em cada referência para obter um relatório de análise, comparar os invariantes calculados por IKOS e PIKOS ou medir a aceleração entre IKOS e PIKOS. Além disso, pode -se reproduzir os dados e gerar tabelas e figuras no papel.
Como o artigo executa os experimentos em 4330 benchmarks, recomenda -se o ambiente de computação em nuvem para reproduzir os resultados em tempo hábil. Configurações e scripts detalhados da AWS usados pelos autores são fornecidos no aws/ .
O ambiente de referência usa Ubuntu 16.04 .
Pule a seção de instalação se você estiver usando o Docker. Precisa docker instalado. A imagem está disponível no repositório DockerHub skkeem/pikos:dev . O comando a seguir baixará a imagem e executará IT INTERACTIVLEY:
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256: 3D99811735E0E3577E7EEAEA90785323D1975AC6250939BA4F70E6695EBEDF5520
Pode -se também construir a imagem usando o Dockerfile neste repositório.
$ docker build -t skkeem/pikos:dev .
O script install_dependencies.sh instalará todas as dependências necessárias. Requer acesso raiz.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
Dependências:
Python3.6 Dependências:
O script install.sh comprará e instalará Pikos no diretório ./build/ . Não requer acesso raiz.
$ ./install.sh
O Script extract_benchmarks.sh extrairá os benchmarks no diretório ./benchmarks/ . Não requer acesso raiz. O SHA256SUM do arquivo baixado é D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EEE9266F6B1B1C1.
$ ./extract_benchmarks.sh
O script run_pikos.sh executa a análise no programa fornecido. Ele calcula os invariantes e executa verificações neles. Esse script é apenas para ilustrar que o Pikos está funcionando totalmente intérprete abstrato e não é usado ou necessário na reprodução dos resultados.
$ ./run_pikos.sh ./benchmarks/test.c
Se você vir a seguinte saída como resultado, a instalação foi bem -sucedida e agora você pode reproduzir os resultados. Pikos relata duas ocorrências de transbordamento de buffer na linha 8 e 9.
[*] Compiling ./benchmarks/test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] (Concurrently) Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.056 sec
ikos-analyzer: 0.019 sec
ikos-pp : 0.011 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
benchmarks/test.c: In function 'main':
benchmarks/test.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
benchmarks/test.c: In function 'main':
benchmarks/test.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
Pikos herda as opções de linha de comando dos IKOS. Abaixo destaca as opções relevantes usadas neste artefato. Descrição dos domínios resumo numéricos são retirados da documentação do IKOS.
O uso do parâmetro -nt restringe o número de threads permitidos em Pikos. O comando a seguir executará Pikos com o máximo de 4 threads:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 é o padrão. -nt=0 permitirá que a biblioteca TBB decida o número de threads. Os autores arbitrários escolheram 99 como o número máximo de threads. Para alterar isso, modifique a linha 991 de ./pikos/analyzer/src/ikos_analyzer.cpp e instale novamente.
O uso do parâmetro -cs restringe a sensibilidade do contexto em Pikos. Esse número corresponde à profundidade permitida de conslinação dinâmica na análise interprocedural. O comando a seguir executará Pikos com o máximo de 5 chamadas de profundidade de função:
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0 é o padrão e desativa essa restrição. Essa restrição é usada apenas para os benchmarks que levam mais de 4 horas para analisar. Consulte benchmarks/README.md para obter mais detalhes.
A lista de domínios resumidos numéricos disponíveis (seguros para threads) são:
-d=interval : o domínio do intervalo, consulte CC77.-d=congruence : o domínio da congruência, veja Gra89.-d=interval-congruence : o produto reduzido de intervalo e congruência.-d=dbm : o domínio das matrizes ligadas à diferença, consulte Pado01.-d=gauge : o domínio do medidor, consulte Cav12.-d=gauge-interval-congruence : o produto reduzido de medidor, intervalo e congruência. Por padrão, Pikos usa o domínio intervalado e as experiências foram realizadas com ele. Se você quiser experimentar outros domínios, use o parâmetro -d :
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Passando as opções, --no-checks --no-fixpoint-cache , desativa os cheques-como análise de transbordamento de buffer, divisão por análise zero, análise de ponteiro nulo, etc-depois de calcular os invariantes:
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Eles são aprovados ao cronometrar os resultados , pois estamos preocupados apenas com o tempo de computação invariante.
Para -nt acima de 99, a comparação entre IKOS e PIKOS será realizada em vez da análise regular. Por exemplo, passar -nt=104 calculará e comparará os invariantes de IKOS e PIKOS com o máximo de 4 threads. Se os invariantes diferirem, "Infundir !!" será impresso e o processo retornará 42. Todas as execuções usando os domínios abstratos acima devem ter os mesmos invariantes por design.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
Reproduzindo os resultados são divididos em etapas: (1) reproduzindo os dados e (2) gerando tabelas/figuras a partir dos dados. O primeiro passo pode levar muito tempo se você optar por reproduzir todos os dados. Esta etapa pode ser feita usando a AWS para terminar em tempo hábil. Consulte aws/README.md para obter mais informações. O segundo passo não deve levar muito tempo e pode ser feito localmente. Ainda exige que as dependências sejam instaladas localmente. Consulte install_dependencies.sh .
Novamente, a aceleração de Pikos vem da utilização de vários núcleos da CPU. O PIKOS exige que as máquinas de vários núcleos reproduzam os resultados. Requer pelo menos 16 núcleos para reproduzir todos os resultados. Para os scripts com o nome de reproduce*.sh , especificaremos a menor quantidade de núcleos necessários no final dos nomes.
Além disso, o uso do TCMalloc , que é um alocador de memória instalado em install_dependencies.sh , é uma obrigação na reprodução dos resultados. Verifique se ele está instalado corretamente. Deve haver uma biblioteca, /usr/local/lib/libtcmalloc.so .
Um script opcional, measure_speedup.sh , é fornecido para medir a aceleração de uma única referência. Ele leva as mesmas opções de linha de comando que run_pikos.sh . Simplesmente produz a aceleração, definida como o tempo de execução do IKOS / tempo de execução do Pikos.
$ ./measure_speedup.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
>>> Running time of IKOS = 31.33911 seconds.
>>> Running time of PIKOS = 10.12769 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS) = 3.09x.
Os scripts a seguir geram dados em um arquivo CSV. Possui as seguintes colunas:
benchmark : Nome da referência.category : a fonte da referência. SVC ou OSS.cs : a sensibilidade do contexto usada.walltime (s) : tempo de análise em ikoswalltime (s)-k : Tempo de análise em Pikos, onde K é o número de threads permitidos.speedup-k : Speedup of PikosIgnore avisos sobre nenhum arquivo de propriedade, substituição variável e nome do arquivo aparecendo duas vezes ao executar os scripts.
Ele administra Ikos, Pikos <2>, Pikos <4>, Pikos <6> e Pikos <8> em todos os benchmarks. Ele produz all.csv . Isso leva muito tempo (aproximadamente 48 dias, se estiver usando apenas uma única máquina).
$ ./reproduce_all-8.sh
Ele é executado ikos e pikos <4> em todos os benchmarks. Ele produz rq1.csv . Isso pode ser usado para responder RQ1. Isso também leva muito tempo (aproximadamente 25 dias, se estiver usando apenas uma única máquina).
$ ./reproduce_rq1-4.sh
Ele é executado IKOS e PIKOS <4> em benchmarks na Tabela 3. É produz tab2.csv . Isso pode ser usado para gerar a Tabela 2. Isso leva cerca de 36 horas, se estiver usando apenas uma única máquina.
$ ./reproduce_tab2-4.sh
Como alternativa, pode -se optar por executar apenas a parte superior da Tabela 2. Ele produz tab2a.csv . Isso leva cerca de 8 horas, se estiver usando apenas uma única máquina.
$ ./reproduce_tab2a-4.sh
O comando a seguir mede a aceleração para a referência com maior aceleração em Pikos <4>. O resultado para este benchmark pode ser encontrado na primeira entrada da Tabela 2.
$ ./measure_speedup.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/aureport.bc
>>> Running time of IKOS = 684.19316 seconds.
>>> Running time of PIKOS = 188.25443 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS) = 3.63x.
Ele é executado IKOS, PIKOS <4>, Pikos <8>, Pikos <12> e Pikos <16> em benchmarks na Tabela 3. É produz tab3.csv . Isso pode ser usado para gerar a Tabela 3. Isso leva aproximadamente 12 horas, se estiver usando apenas uma única máquina.
$ ./reproduce_tab3-16.sh
O comando a seguir mede as acelerações para a referência com maior escalabilidade, ./benchmarks/OSS/audit-2.8.4/aureport.bc/ . O resultado para este benchmark pode ser encontrado na primeira entrada da Tabela 3.
$ ./measure_tab3-aureport.sh
>>> Running time of IKOS = 684.19316 seconds.
>>> Running time of PIKOS<4> = 188.25443 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<4>) = 3.63x.
>>> Running time of PIKOS<8> = 104.18474 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<8>) = 6.57x.
>>> Running time of PIKOS<12> = 75.86368 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<12>) = 9.02x.
>>> Running time of PIKOS<16> = 62.36445 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<16>) = 10.97x.
O arquivo CSV produzido acima pode ser usado para gerar tabelas e figuras no papel. Demonstraremos com os dados obtidos pelos autores em ./results-paper/all.csv , que podem ser reproduzidos usando o script descrito em reproduzir tudo.
O script generate_fig5.py gera o gráfico de dispersão na Fig. 5. Ele também produz as médias descritas na seção de avaliação. Requer as colunas walltime (s) , walltime (s)-4 e speedup-4 no arquivo CSV. Ele produz fig5.png .
$ ./generate_fig5.py ./results-paper/all.csv
O script generate_fig6.py gera os histogramas na Fig. 6. Requer as colunas walltime (s) , walltime (s)-4 e speedup-4 no arquivo CSV. Ele gera 4 subfiguras, fig6-[0~3].png .
$ ./generate_fig6.py ./results-paper/all.csv
O script generate_fig9.py gera gráfico de caixa e gráfico de violino na Fig. 7. Requer as colunas walltime (s) , speedup-2 , speedup-4 , speedup-6 e speedup-8 no arquivo CSV. Ele produz fig7-a.png e fig7-b.png .
$ ./generate_fig7.py ./results-paper/all.csv
O script generate_fig8.py gera gráfico de coeficiente de escalabilidade na Fig. 8. Requer as colunas walltime (s) , speedup-2 , speedup-4 , speedup-6 e speedup-8 no arquivo CSV. Ele produz fig8-a.png e fig8-b.png .
$ ./generate_fig8.py ./results-paper/all.csv
O script generate_tab3.py gera as entradas para a Tabela 2. Requer o benchmark colunas, category , walltime (s) , walltime (s)-4 e speedup-4 no arquivo CSV. Ele produz tab2-speedup.csv e tab2-ikos.csv , que são usados para preencher a Tabela 2.
$ ./generate_tab2.py ./results-paper/all.csv
O script generate_tab4.py escolhe os benchmarks para a Tabela 3 com base no coeficiente de escalabilidade. Requer o benchmark colunas, category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 e speedup-8 no arquivo CSV. Ele gera tab3-candidates.csv . É preciso executar Pikos <12> e Pikos <16> nesses benchmarks adicionalmente para completar a Tabela 3.
$ ./generate_tab3.py ./results-paper/all.csv
