Scheduling policy for efficient parallelization of software analysis in a distributed computing environment

An article of manufacture comprising:

• a non-transitory computer readable medium;
• and
• computer-executable instructions carried on the non-transitory computer readable medium, the instructions readable by a processor, the instructions, when read and executed, for causing the processor to:
• access a job queue, the job queue comprising an indication of one or more jobs to be executed by a worker node, each job indicating a portion of a code to be verified;
• access a resource queue, the resource queue comprising an indication of one or more worker nodes available to verify a portion of software;
• and
• when an addition is made to a job queue or to a resource queue, assign a job from the job queue to a resource from the resource queue;
• wherein the resource is selected by determining the best match for the characteristics of selected job among the resources in the resource queue, comprising the determining which resource comprises the lowest initialization cost for the selected job.

An electronic device comprising:

• a memory comprising a job queue and a resource queue, wherein:
• the job queue comprises an indication of one or more jobs to be executed by a worker node, each job indicating a portion of code to be verified;
• and
• the resource queue comprises an indication of one or more worker nodes available to verify a portion of code to be verified;
• and
• a processor coupled to the memory;
• wherein the processor is configured to:
• access the job queue;
• access the resource queue;
• and
• when an addition is made to a job queue or to a resource queue, assign a job from the job queue to a resource from the resource queue;
• wherein the resource is selected by determining the best match for the characteristics of the selected job among the resources in the resource queue, comprising determining which resource comprises the lowest initialization cost for the selected job.