<commit_before>
module Bpl
  module AST

    class Program

      def verify(options = {})
        if options[:incremental] && options[:parallel]
          verify_incremental_in_parallel options
        elsif options[:incremental]
          verify_incremental options
        else
          verify_one_shot options
        end
      end

      def verify_one_shot(options = {})
        unroll = options[:unroll]
        delays = options[:delays]
        if trace = vvvvv(options)
          puts "Got a trace w/ depth #{unroll || "inf."} and #{delays} delays." unless $quiet
        else
          puts "Verified w/ depth #{unroll || "inf."} and #{delays} delays." unless $quiet
        end
        return trace
      end

      def verify_incremental(options = {})
        unroll_bound = options[:unroll] || Float::INFINITY
        delay_bound = options[:delays] || Float::INFINITY

        unroll = 0
        delays = 0

        while true
          Kernel::print "Verifying w/ depth #{unroll} and #{delays} delays..." unless $quiet
          Kernel::print "\r" unless $quiet

          break if trace = vvvvv(options.merge(unroll: unroll, delays: delays))
          break if delays >= delay_bound && unroll >= unroll_bound

          if (delays < delay_bound && delays < unroll) || unroll >= unroll_bound
            delays += 1
          else
            unroll += 1
          end
        end

        if trace
          puts "Got a trace w/ depth #{unroll} and #{delays} delays." unless $quiet
        else
          puts "Verified up to depth #{unroll} w/ #{delays} delays." unless $quiet
        end

        return trace
      end

      def verify_incremental_in_parallel(options = {})
        unroll_bound = options[:unroll] || Float::INFINITY
        delay_bound = options[:delays] || Float::INFINITY

        done = 0

        unroll_lower = 0
        delay_lower = 0

        tasks = [nil, nil]
        start = Time.now
        trace = nil

        EventMachine.run do
          EventMachine.add_periodic_timer(0.5) do
            Kernel::print \
              "Verifying in parallel w/ unroll/delays " \
              "#{tasks[0] ? "#{tasks[0][:unroll]}/#{tasks[0][:delays]}" : "-/-"} " \
                "(#{tasks[0] ? (Time.now - tasks[0][:time]).round : "-"}s) and " \
              "#{tasks[1] ? "#{tasks[1][:unroll]}/#{tasks[1][:delays]}" : "-/-"} " \
                "(#{tasks[1] ? (Time.now - tasks[1][:time]).round : "-"}s) " \
              "total #{(Time.now - start).round}s" \
              "\r" unless $quiet
          end

          (0..1).each do |i|
            EventMachine.defer do
              while true
                unroll = unroll_lower
                delays = delay_lower
                mode = tasks[i] ? tasks[i][:mode] : (i == 0 && :unroll || i == 1 && :delay)
                mode = :unroll if delays == delay_bound
                mode = :delay if unroll == unroll_bound
                unroll += 1 if mode == :unroll
                delays += 1 if mode == :delay
                if unroll > unroll_bound || delays > delay_bound
                  tasks[i] = nil
                  break
                end
                tasks[i] = {mode: mode, time: Time.now, unroll: unroll, delays: delays}

                if trace = vvvvv(options.merge(unroll: unroll, delays: delays)) then
                  EventMachine.stop
                  puts unless $quiet
                  puts "Got a trace w/ depth #{unroll} and #{delays} delays." unless $quiet
                  break
                end
                unroll_lower += 1 if i == 0
                delay_lower += 1 if i == 1
              end
              if (done += 1) >= 2
                EventMachine.stop
                puts unless $quiet
              end
            end
          end
        end

        puts "Verified up to depth #{unroll_bound} w/ #{delay_bound} delays." \
          unless trace || $quiet

        return trace
      end

      # def verify_incremental_in_parallel(options = {})
      #   unroll_bound = options[:unroll] || Float::INFINITY
      #   delay_bound = options[:delays] || Float::INFINITY
      # 
      #   done = 0
      # 
      #   covered = []
      #   worklist = [{unroll: 0, delays: 0}, {unroll: 1, delays: 0}]
      # 
      #   # EventMachine.threadpool_size = 2
      #   EventMachine.run do
      #     (1..2).each do
      #       EventMachine.defer do
      #         while true
      #           work = worklist.shift
      #           break unless work
      #           unroll = work[:unroll]
      #           delays = work[:delays]
      #           break if covered.any?{|w| w[:unroll] >= unroll && w[:delays] >= delays}
      #           covered.reject!{|w| w[:unroll] <= unroll && w[:delays] <= delays}
      #           covered << work
      # 
      #           puts "Verifying w/ #{unroll} unroll and #{delays} delays." unless $quiet
      #           if vvvvv(options.merge(unroll: unroll, delays: delays)) then
      #             EventMachine.stop
      #             puts "Got a trace..." unless $quiet
      #             break
      #           else
      #             worklist.reject!{|w| w[:unroll] <= unroll && w[:delays] <= delays}
      #             worklist << {unroll: unroll+1, delays: delays} if unroll < unroll_bound
      #             worklist << {unroll: unroll, delays: delays+1} if delays < delay_bound
      #           end
      #         end
      #         EventMachine.stop if (done += 1) >= 2
      #       end
      #     end
      #   end
      # end

      def vvvvv(options = {})
        boogie_opts = []

        orig = source_file || "a.bpl"
        base = File.basename(orig).chomp(File.extname(orig))
        $temp << src = "#{base}.c2s.#{Time.now.to_f}.bpl"
        $temp << model_file = src.chomp('.bpl') + '.model'
        $temp << trace_file = src.chomp('.bpl') + '.trace'
<commit_msg>Trying the worklist parallel algorithm.<commit_after>
module Bpl
  module AST

    class Program

      def verify(options = {})
        if options[:incremental] && options[:parallel]
          verify_parallel_accelerated options
        elsif options[:incremental]
          verify_incremental options
        else
          verify_one_shot options
        end
      end

      def verify_one_shot(options = {})
        unroll = options[:unroll]
        delays = options[:delays]
        if trace = vvvvv(options)
          puts "Got a trace w/ depth #{unroll || "inf."} and #{delays} delays." unless $quiet
        else
          puts "Verified w/ depth #{unroll || "inf."} and #{delays} delays." unless $quiet
        end
        return trace
      end

      def verify_incremental(options = {})
        unroll_bound = options[:unroll] || Float::INFINITY
        delay_bound = options[:delays] || Float::INFINITY

        unroll = 0
        delays = 0

        while true
          Kernel::print "Verifying w/ depth #{unroll} and #{delays} delays..." unless $quiet
          Kernel::print "\r" unless $quiet

          break if trace = vvvvv(options.merge(unroll: unroll, delays: delays))
          break if delays >= delay_bound && unroll >= unroll_bound

          if (delays < delay_bound && delays < unroll) || unroll >= unroll_bound
            delays += 1
          else
            unroll += 1
          end
        end

        if trace
          puts "Got a trace w/ depth #{unroll} and #{delays} delays." unless $quiet
        else
          puts "Verified up to depth #{unroll} w/ #{delays} delays." unless $quiet
        end

        return trace
      end

      def verify_parallel_accelerated(options = {})
        unroll_bound = options[:unroll] || Float::INFINITY
        delay_bound = options[:delays] || Float::INFINITY

        done = 0

        unroll_lower = 0
        delay_lower = 0

        tasks = [nil, nil]
        start = Time.now
        trace = nil

        EventMachine.run do
          EventMachine.add_periodic_timer(0.5) do
            Kernel::print \
              "Verifying in parallel w/ unroll/delays " \
              "#{tasks[0] ? "#{tasks[0][:unroll]}/#{tasks[0][:delays]}" : "-/-"} " \
                "(#{tasks[0] ? (Time.now - tasks[0][:time]).round : "-"}s) and " \
              "#{tasks[1] ? "#{tasks[1][:unroll]}/#{tasks[1][:delays]}" : "-/-"} " \
                "(#{tasks[1] ? (Time.now - tasks[1][:time]).round : "-"}s) " \
              "total #{(Time.now - start).round}s" \
              "\r" unless $quiet
          end

          (0..1).each do |i|
            EventMachine.defer do
              while true
                unroll = unroll_lower
                delays = delay_lower
                mode = tasks[i] ? tasks[i][:mode] : (i == 0 && :unroll || i == 1 && :delay)
                mode = :unroll if delays == delay_bound
                mode = :delay if unroll == unroll_bound
                unroll += 1 if mode == :unroll
                delays += 1 if mode == :delay
                if unroll > unroll_bound || delays > delay_bound
                  tasks[i] = nil
                  break
                end
                tasks[i] = {mode: mode, time: Time.now, unroll: unroll, delays: delays}

                if trace = vvvvv(options.merge(unroll: unroll, delays: delays)) then
                  EventMachine.stop
                  puts unless $quiet
                  puts "Got a trace w/ depth #{unroll} and #{delays} delays." unless $quiet
                  break
                end
                unroll_lower += 1 if i == 0
                delay_lower += 1 if i == 1
              end
              if (done += 1) >= 2
                EventMachine.stop
                puts unless $quiet
              end
            end
          end
        end

        puts "Verified up to depth #{unroll_bound} w/ #{delay_bound} delays." \
          unless trace || $quiet

        return trace
      end

      def verify_parallel_worklist(options = {})
        unroll_bound = options[:unroll] || Float::INFINITY
        delay_bound = options[:delays] || Float::INFINITY

        covered = []
        worklist = [{unroll: 0, delays: 0}, {unroll: 1, delays: 0}]
        tasks = [nil, nil]
        start = Time.now
        trace = nil
        idle = 0

        # EventMachine.threadpool_size = 2
        EventMachine.run do
          EventMachine.add_periodic_timer(0.5) do
            Kernel::print \
              "Verifying in parallel w/ unroll/delays " \
              "#{tasks[0] ? "#{tasks[0][:unroll]}/#{tasks[0][:delays]}" : "-/-"} " \
                "(#{tasks[0] ? (Time.now - tasks[0][:time]).round : "-"}s) and " \
              "#{tasks[1] ? "#{tasks[1][:unroll]}/#{tasks[1][:delays]}" : "-/-"} " \
                "(#{tasks[1] ? (Time.now - tasks[1][:time]).round : "-"}s) " \
              "total #{(Time.now - start).round}s" \
              "\r" unless $quiet
          end

          (0..1).each do |i|
            EventMachine.defer do
              while true
                work = worklist.shift
                break unless work
                unroll = work[:unroll]
                delays = work[:delays]
                next if covered.any?{|w| w[:unroll] >= unroll && w[:delays] >= delays}
                covered.reject!{|w| w[:unroll] <= unroll && w[:delays] <= delays}
                covered << work

                tasks[i] = {time: Time.now, unroll: unroll, delays: delays}

                if trace = vvvvv(options.merge(unroll: unroll, delays: delays)) then
                  EventMachine.stop
                  puts unless $quiet
                  puts "Got a trace w/ depth #{unroll} and #{delays} delays." unless $quiet
                  break
                else
                  worklist.reject!{|w| w[:unroll] <= unroll && w[:delays] <= delays}
                  worklist << {unroll: unroll+1, delays: delays} if unroll < unroll_bound
                  worklist << {unroll: unroll, delays: delays+1} if delays < delay_bound
                end
              end
              tasks[i] = nil
              EventMachine.stop if (idle += 1) >= 2
            end
          end
        end

        puts "Verified up to depth #{unroll_bound} w/ #{delay_bound} delays." \
          unless trace || $quiet
        return trace
      end

      def vvvvv(options = {})
        boogie_opts = []

        orig = source_file || "a.bpl"
        base = File.basename(orig).chomp(File.extname(orig))
        $temp << src = "#{base}.c2s.#{Time.now.to_f}.bpl"
        $temp << model_file = src.chomp('.bpl') + '.model'
        $temp << trace_file = src.chomp('.bpl') + '.trace'

{'fraction_non_alphanumeric': 0.12830098631880368, 'fraction_numerical': 0.007954183900731784, 'mean_word_length': 1.5151030206041207, 'pattern_counts': {'":': 0, '<': 43, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '646611', 'n_tokens_mistral': 3883, 'n_tokens_neox': 3629, 'n_words': 957}