Testes do KEMS em Lote

Configuração

• Máquina: xue.dainf.ct.utfpr.edu.br
• Servidor git

Como descobrir a configuração da máquina usada para testes no Linux

Em destaque nas linha abaixo os itens mais importantes. Ver mais em http://www.linux.com/archive/feature/126718?theme=print

Sistema Operacional

• Comando: cat /proc/version

• Exemplo:

cat /proc/version 
Linux version 2.6.18-4-486 (Debian 2.6.18.dfsg.1-12etch2) (dannf@debian.org) (gcc version 4.1.2 20061115 (prerelease) (Debian 4.1.1-21)) #1 Wed May 9 22:23:40 UTC 2007

Ou uname -a

CPU

• Comando: cat /proc/cpuinfo

• Exemplo:

adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/cpuinfo 
processor	: 0
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 47
model name	: AMD Athlon(tm) 64 Processor 3000+
stepping	: 2
cpu MHz		: 1800.204
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 syscall nx mmxext fxsr_opt lm 3dnowext 3dnow pni lahf_lm ts fid vid ttp tm stc
bogomips	: 3602.35

Memória

• Comando: cat /proc/meminfo

• Exemplo:

adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/meminfo 
MemTotal:       508596 kB
(...)
VmallocChunk:   517824 kB

Roteiro

• Editar arquivo de sequencia <arquivo.seq>.

• Executar da seguinte forma:

java -jar kems.jar <arquivo.seq>

• Para direcionar para arquivo:

java -jar kems.jar <arquivo.seq> > [results.tex]

• Para deixar em background (e assim poder deslogar e deixar rodando):

nohup java -jar kems.jar <arquivo.seq> > results.tex &

• Neste caso, acompanhar a execução do processo encontrando-o em

ps -aux | grep java

ou

top

ou

tail -f [results.tex]

Como elaborar sequencias de testes

Basta editar o arquivo .seq:

  nano teste.lfi.seq

E selecionar as famílias a serem provadas em 'problems':

  parser=satlfiinconsdef
  saveOrigin=true
  discardClosedBranches=false
  saveDiscardedBranches=false
  times=1
  timeLimit=10

  problems=
  problems/generated/lfiProblems/family5/family5_05.prove
  problems/generated/lfiProblems/family5/family5_10.prove
  problems/generated/lfiProblems/family5/family5_15.prove

  strategies=
  C1SimpleStrategy

  comparators=
  InsertionOrderComparator
  ReverseInsertionOrderComparator
  #AndComparator

TODO: Como decidir quantas vezes rodar cada caso

Ao editar o arquivo .seq:

  nano teste.lfi.seq

Adicionar o número de vezes em 'times' (no caso esta como 1):

  parser=satlfiinconsdef
  saveOrigin=true
  discardClosedBranches=false
  saveDiscardedBranches=false
  times=1
  timeLimit=10

  problems=
  problems/generated/lfiProblems/family5/family5_05.prove
  problems/generated/lfiProblems/family5/family5_10.prove
  problems/generated/lfiProblems/family5/family5_15.prove

  strategies=
  C1SimpleStrategy

  comparators=
  InsertionOrderComparator
  ReverseInsertionOrderComparator
  #AndComparator